replace codomain by codomain/range for onto functions

as remarked by JK

set.mm

@@ -64074,8 +64074,8 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
     CKUFUDTAUCCLMNOPABCRBAUARS $.
 
   $( A relation is a one-to-one onto function iff its converse is a one-to-one
-     onto function with domain and codomain interchanged.  (Contributed by NM,
-     8-Dec-2003.) $)
+     onto function with domain and codomain/range interchanged.  (Contributed
+     by NM, 8-Dec-2003.) $)
   f1ocnvb $p |- ( Rel F ->
                 ( F : A -1-1-onto-> B <-> `' F : B -1-1-onto-> A ) ) $=
     ( wrel wf1o ccnv f1ocnv wceq wb dfrel2 f1oeq1 sylbi syl5ib impbid2 ) CDZABC
@@ -76850,8 +76850,8 @@ as a separate axiom in an axiom system (such as Kunen's) that uses this
     ex focdmex syl6ci imp ) ABDEZBCFZAGFZUDUEDHZGFZUGADIZJZUFUDUEUHUDUGBKUEUHUD
     ABDABDLMUGBCNOTUDUGAUIPUJABDQUGAUIRSUGAGUIUAUBUC $.
 
-  $( The codomain of a 1-1 onto function is a set iff its domain is a set.
-     (Contributed by AV, 21-Mar-2019.) $)
+  $( The codomain/range of a 1-1 onto function is a set iff its domain is a
+     set.  (Contributed by AV, 21-Mar-2019.) $)
   f1ovv $p |- ( F : A -1-1-onto-> B -> ( A e. _V <-> B e. _V ) ) $=
     ( wf1o cvv wcel wfo f1ofo focdmex syl5com wf1 wi f1of1 f1dmex ex syl impbid
     ) ABCDZAEFZBEFZRABCGSTABCHABECIJRABCKZTSLABCMUATSABECNOPQ $.