diff --git a/changes-set.txt b/changes-set.txt
index 2e86dc4519..c285150cca 100644
--- a/changes-set.txt
+++ b/changes-set.txt
@@ -87,6 +87,12 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+13-Jan-25 elunnel2  [same]      moved from GS's mathbox to main set.mm
+12-Jan-25 rimrhm    [same]      revised - eliminated unnecessary hypotheses
+12-Jan-25 isrim     [same]      revised - eliminated unnecessary antecedent
+12-Jan-25 isrim0    [same]      revised - eliminated unnecessary antecedent
+12-Jan-25 elrnust   ---         obsolete - use elfvunirn instead
+12-Jan-25 elunirn2  ---         obsolete - use elfvunirn instead
 12-Jan-25 ---       ---         Moved surreal birthday and density theorems
                                 from SF's mathbox to main set.mm
 12-Jan-25 sotrine   [same]      Moved from SF's mathbox to main set.mm
@@ -157,7 +163,7 @@ Date      Old       New         Notes
 13-Dec-24 wksonproplem [same]   revised - eliminated hypothesis
 13-Dec-24 mptmpoopabovd [same]  revised - eliminated hypotheses
 13-Dec-24 mptmpoopabbrd [same]  revised - eliminated hypotheses
-13-Dec-24 wlkRes     ---        obsolete - use obapresex2 instead
+13-Dec-24 wlkRes     ---        obsolete - use opabresex2 instead
 13-Dec-24 opabresex2d ---       obsolete - use opabresex2 instead
 27-Nov-24 eldifsucnn [same]     moved from SF's mathbox to main set.mm
 27-Nov-24 nnasmo    [same]      moved from SF's mathbox to main set.mm
diff --git a/discouraged b/discouraged
index 74c9b6e58e..c9ee03edf9 100644
--- a/discouraged
+++ b/discouraged
@@ -9063,6 +9063,7 @@
 "ispsubclN" is used by "pmapsubclN".
 "ispsubclN" is used by "psubcli2N".
 "ispsubclN" is used by "psubcliN".
+"isrim0OLD" is used by "isrimOLD".
 "isrngo" is used by "isrngod".
 "isrngo" is used by "rngoi".
 "isrngod" is used by "iscringd".
@@ -16544,6 +16545,7 @@ New usage of "elreal" is discouraged (7 uses).
 New usage of "elreal2" is discouraged (3 uses).
 New usage of "elringchomALTV" is discouraged (1 uses).
 New usage of "elrngchomALTV" is discouraged (1 uses).
+New usage of "elrnustOLD" is discouraged (0 uses).
 New usage of "elsetrecslem" is discouraged (1 uses).
 New usage of "elspancl" is discouraged (1 uses).
 New usage of "elspani" is discouraged (2 uses).
@@ -16555,6 +16557,7 @@ New usage of "elspansn5" is discouraged (2 uses).
 New usage of "elspansncl" is discouraged (1 uses).
 New usage of "elspansni" is discouraged (2 uses).
 New usage of "eltpsgOLD" is discouraged (0 uses).
+New usage of "elunirn2OLD" is discouraged (0 uses).
 New usage of "elunirnALT" is discouraged (0 uses).
 New usage of "elunop" is discouraged (7 uses).
 New usage of "elunop2" is discouraged (0 uses).
@@ -16746,10 +16749,12 @@ New usage of "funopg" is discouraged (0 uses).
 New usage of "funopsn" is discouraged (2 uses).
 New usage of "fvimacnvALT" is discouraged (0 uses).
 New usage of "fvmptopabOLD" is discouraged (0 uses).
+New usage of "fvn0fvelrnOLD" is discouraged (0 uses).
 New usage of "fvpr1OLD" is discouraged (0 uses).
 New usage of "fvpr2OLD" is discouraged (0 uses).
 New usage of "fvpr2gOLD" is discouraged (0 uses).
 New usage of "fvprcALT" is discouraged (0 uses).
+New usage of "fvssunirnOLD" is discouraged (0 uses).
 New usage of "gcdabsOLD" is discouraged (0 uses).
 New usage of "gen11" is discouraged (19 uses).
 New usage of "gen11nv" is discouraged (5 uses).
@@ -17395,6 +17400,7 @@ New usage of "ipval3" is discouraged (1 uses).
 New usage of "ipz" is discouraged (1 uses).
 New usage of "isablo" is discouraged (3 uses).
 New usage of "isabloi" is discouraged (3 uses).
+New usage of "isanmbfmOLD" is discouraged (0 uses).
 New usage of "isarep1OLD" is discouraged (0 uses).
 New usage of "isass" is discouraged (1 uses).
 New usage of "isblo" is discouraged (5 uses).
@@ -17448,6 +17454,8 @@ New usage of "ispointN" is discouraged (2 uses).
 New usage of "isposixOLD" is discouraged (0 uses).
 New usage of "ispsubcl2N" is discouraged (0 uses).
 New usage of "ispsubclN" is discouraged (10 uses).
+New usage of "isrim0OLD" is discouraged (1 uses).
+New usage of "isrimOLD" is discouraged (0 uses).
 New usage of "isrngo" is discouraged (2 uses).
 New usage of "isrngod" is discouraged (1 uses).
 New usage of "issgrpALT" is discouraged (1 uses).
@@ -17744,6 +17752,7 @@ New usage of "matvscaOLD" is discouraged (0 uses).
 New usage of "max1ALT" is discouraged (0 uses).
 New usage of "mayete3i" is discouraged (1 uses).
 New usage of "mayetes3i" is discouraged (0 uses).
+New usage of "mbfmbfmOLD" is discouraged (0 uses).
 New usage of "mdbr" is discouraged (6 uses).
 New usage of "mdbr2" is discouraged (7 uses).
 New usage of "mdbr3" is discouraged (0 uses).
@@ -18856,6 +18865,7 @@ New usage of "riesz2" is discouraged (0 uses).
 New usage of "riesz3i" is discouraged (2 uses).
 New usage of "riesz4" is discouraged (4 uses).
 New usage of "riesz4i" is discouraged (1 uses).
+New usage of "rimrhmOLD" is discouraged (0 uses).
 New usage of "ringcbasALTV" is discouraged (7 uses).
 New usage of "ringcbasbasALTV" is discouraged (3 uses).
 New usage of "ringccatALTV" is discouraged (5 uses).
@@ -20431,7 +20441,9 @@ Proof modification of "elpwgdedVD" is discouraged (23 steps).
 Proof modification of "elpwi2OLD" is discouraged (21 steps).
 Proof modification of "elrabiOLD" is discouraged (55 steps).
 Proof modification of "elrefsymrels3" is discouraged (65 steps).
+Proof modification of "elrnustOLD" is discouraged (4 steps).
 Proof modification of "eltpsgOLD" is discouraged (73 steps).
+Proof modification of "elunirn2OLD" is discouraged (65 steps).
 Proof modification of "elunirnALT" is discouraged (38 steps).
 Proof modification of "en0ALT" is discouraged (62 steps).
 Proof modification of "en0OLD" is discouraged (86 steps).
@@ -20705,10 +20717,12 @@ Proof modification of "funmoOLD" is discouraged (115 steps).
 Proof modification of "fvilbdRP" is discouraged (27 steps).
 Proof modification of "fvimacnvALT" is discouraged (102 steps).
 Proof modification of "fvmptopabOLD" is discouraged (185 steps).
+Proof modification of "fvn0fvelrnOLD" is discouraged (94 steps).
 Proof modification of "fvpr1OLD" is discouraged (56 steps).
 Proof modification of "fvpr2OLD" is discouraged (44 steps).
 Proof modification of "fvpr2gOLD" is discouraged (75 steps).
 Proof modification of "fvprcALT" is discouraged (26 steps).
+Proof modification of "fvssunirnOLD" is discouraged (47 steps).
 Proof modification of "gcdabsOLD" is discouraged (170 steps).
 Proof modification of "gen11" is discouraged (27 steps).
 Proof modification of "gen11nv" is discouraged (14 steps).
@@ -20813,6 +20827,7 @@ Proof modification of "intprgOLD" is discouraged (80 steps).
 Proof modification of "iotaexOLD" is discouraged (57 steps).
 Proof modification of "iotassuniOLD" is discouraged (35 steps).
 Proof modification of "iotavalOLD" is discouraged (101 steps).
+Proof modification of "isanmbfmOLD" is discouraged (15 steps).
 Proof modification of "isarep1OLD" is discouraged (106 steps).
 Proof modification of "iscmgmALT" is discouraged (57 steps).
 Proof modification of "iscsgrpALT" is discouraged (57 steps).
@@ -20822,6 +20837,8 @@ Proof modification of "ismgmALT" is discouraged (53 steps).
 Proof modification of "ismgmOLD" is discouraged (292 steps).
 Proof modification of "isosctrlem1ALT" is discouraged (363 steps).
 Proof modification of "isposixOLD" is discouraged (72 steps).
+Proof modification of "isrim0OLD" is discouraged (177 steps).
+Proof modification of "isrimOLD" is discouraged (64 steps).
 Proof modification of "issgrpALT" is discouraged (53 steps).
 Proof modification of "issmgrpOLD" is discouraged (85 steps).
 Proof modification of "istrkg2d" is discouraged (439 steps).
@@ -20858,6 +20875,7 @@ Proof modification of "mathbox" is discouraged (1 steps).
 Proof modification of "matscaOLD" is discouraged (73 steps).
 Proof modification of "matvscaOLD" is discouraged (69 steps).
 Proof modification of "max1ALT" is discouraged (48 steps).
+Proof modification of "mbfmbfmOLD" is discouraged (9 steps).
 Proof modification of "meetcomALT" is discouraged (83 steps).
 Proof modification of "merco1" is discouraged (57 steps).
 Proof modification of "merco1lem1" is discouraged (191 steps).
@@ -21226,6 +21244,7 @@ Proof modification of "rexn0OLD" is discouraged (17 steps).
 Proof modification of "rexprgOLD" is discouraged (17 steps).
 Proof modification of "rexsngOLD" is discouraged (10 steps).
 Proof modification of "rgen2a" is discouraged (81 steps).
+Proof modification of "rimrhmOLD" is discouraged (25 steps).
 Proof modification of "rlimaddOLD" is discouraged (159 steps).
 Proof modification of "rlimmulOLD" is discouraged (159 steps).
 Proof modification of "rmoanidOLD" is discouraged (37 steps).
diff --git a/set.mm b/set.mm
index 33e9d938f8..6da3bd092c 100644
--- a/set.mm
+++ b/set.mm
@@ -38961,11 +38961,16 @@ technically classes despite morally (and provably) being sets, like ` 1 `
       UCACLMDBCNOP $.
   $}
 
-  $( A member of a union that is not member of the first class, is member of
-     the second class.  (Contributed by Glauco Siliprandi, 11-Dec-2019.) $)
+  $( A member of a union that is not a member of the first class, is a member
+     of the second class.  (Contributed by Glauco Siliprandi, 11-Dec-2019.) $)
   elunnel1 $p |- ( ( A e. ( B u. C ) /\ -. A e. B ) -> A e. C ) $=
     ( cun wcel wo elun biimpi orcanai ) ABCDEZABEZACEZJKLFABCGHI $.
 
+  $( A member of a union that is not a member of the second class, is a member
+     of the first class.  (Contributed by Glauco Siliprandi, 11-Dec-2019.) $)
+  elunnel2 $p |- ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B ) $=
+    ( cun wcel wo elun biimpi orcomd orcanai ) ABCDEZACEZABEZKMLKMLFABCGHIJ $.
+
   ${
     $d x A $.  $d x B $.  $d x C $.
     uneqri.1 $e |- ( ( x e. A \/ x e. B ) <-> x e. C ) $.
@@ -64961,10 +64966,35 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
     IAFZDGZHZIUJUIDUMUJJULUMDULUKKDLMNOUJPZUKUMUIUKULSUNBQIZUIQIBUIARZUIUKIUOUJ
     BAUATUNBAUBUPUJUPUJABUCUDTBUIAQQUEUFUGUH $.
 
-  $( The result of a function value is always a subset of the union of the
-     range, even if it is invalid and thus empty.  (Contributed by Stefan
-     O'Rear, 2-Nov-2014.)  (Revised by Mario Carneiro, 31-Aug-2015.) $)
-  fvssunirn $p |- ( F ` X ) C_ U. ran F $=
+  $( If the value of a function is not null, the value is an element of the
+     range of the function.  (Contributed by Alexander van der Vekens,
+     22-Jul-2018.)  (Proof shortened by SN, 13-Jan-2025.) $)
+  fvn0fvelrn $p |- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F ) $=
+    ( cfv c0 wne crn csn cun wcel wn fvrn0 nelsn elunnel2 sylancr ) BACZDEOAFZD
+    GZHIOQIJOPIABKODLOPQMN $.
+
+  $( A function value is a subset of the union of the range.  (An artifact of
+     our function value definition, compare ~ elfvdm ).  (Contributed by
+     Thierry Arnoux, 13-Nov-2016.)  Remove functionhood antecedent.  (Revised
+     by SN, 10-Jan-2025.) $)
+  elfvunirn $p |- ( B e. ( F ` A ) -> B e. U. ran F ) $=
+    ( cfv wcel crn cuni c0 wne wss ne0i fvn0fvelrn elssuni 3syl sseld pm2.43i )
+    BACDZEZBCFZGZERQTBRQHIQSEQTJQBKCALQSMNOP $.
+
+  ${
+    $d F x $.  $d X x $.
+    $( The result of a function value is always a subset of the union of the
+       range, even if it is invalid and thus empty.  (Contributed by Stefan
+       O'Rear, 2-Nov-2014.)  (Revised by Mario Carneiro, 31-Aug-2015.)  (Proof
+       shortened by SN, 13-Jan-2025.) $)
+    fvssunirn $p |- ( F ` X ) C_ U. ran F $=
+      ( vx cfv crn cuni cv elfvunirn ssriv ) CBADAEFBCGAHI $.
+  $}
+
+  $( Obsolete version of ~ fvssunirn as of 13-Jan-2025.  (Contributed by Stefan
+     O'Rear, 2-Nov-2014.)  (Revised by Mario Carneiro, 31-Aug-2015.)
+     (Proof modification is discouraged.)  (New usage is discouraged.) $)
+  fvssunirnOLD $p |- ( F ` X ) C_ U. ran F $=
     ( cfv crn c0 csn cun cuni wcel wss fvrn0 elssuni ax-mp uniun 0ex uneq2i un0
     unisn 3eqtri sseqtri ) BACZADZEFZGZHZUBHZUAUDIUAUEJABKUAUDLMUEUFUCHZGUFEGUF
     UBUCNUGEUFEORPUFQST $.
@@ -67686,10 +67716,10 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
   fvressn $p |- ( X e. V -> ( ( F |` { X } ) ` X ) = ( F ` X ) ) $=
     ( wcel csn snidg fvresd ) CBDCCEACBFG $.
 
-  $( If the value of a function is not null, the value is an element of the
-     range of the function.  (Contributed by Alexander van der Vekens,
-     22-Jul-2018.) $)
-  fvn0fvelrn $p |- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F ) $=
+  $( Obsolete version of ~ fvn0fvelrn as of 13-Jan-2025.  (Contributed by
+     Alexander van der Vekens, 22-Jul-2018.)  (New usage is discouraged.)
+     (Proof modification is discouraged.) $)
+  fvn0fvelrnOLD $p |- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F ) $=
     ( cfv c0 wne cdm wcel csn cres wfun wa crn fvfundmfvn0 wi eldmressnsn pm3.2
     fvelrn syl ex com13 mpd imp fvressn eleq1d fvrnressn sylbid impcom 3syl ) B
     ACZDEBAFZGZABHIZJZKBULCZULLZGZUKKZUIALGZBAMUKUMUQUKBULFGZUMUQNBAOUMUSUKUQUM
@@ -68727,7 +68757,8 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
   ${
     $d x y A $.  $d x y F $.
     $( Membership in the union of the range of a function.  See ~ elunirnALT
-       for a shorter proof which uses ~ ax-pow .  (Contributed by NM,
+       for a shorter proof which uses ~ ax-pow .  See ~ elfvunirn for a more
+       general version of the reverse direction.  (Contributed by NM,
        24-Sep-2006.) $)
     elunirn $p |- ( Fun F ->
                         ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) ) $=
@@ -68754,9 +68785,10 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
 
   ${
     $d x A $.  $d x B $.  $d x F $.
-    $( Condition for the membership in the union of the range of a function.
-       (Contributed by Thierry Arnoux, 13-Nov-2016.) $)
-    elunirn2 $p |- ( ( Fun F /\ B e. ( F ` A ) ) -> B e. U. ran F ) $=
+    $( Obsolete version of ~ elfvunirn as of 12-Jan-2025.  (Contributed by
+       Thierry Arnoux, 13-Nov-2016.)  (New usage is discouraged.)
+       (Proof modification is discouraged.) $)
+    elunirn2OLD $p |- ( ( Fun F /\ B e. ( F ` A ) ) -> B e. U. ran F ) $=
       ( vx wfun cfv wcel wa crn cuni cdm wrex elfvdm wceq eleq2d rspcev mpancom
       cv fveq2 adantl wb elunirn adantr mpbird ) CEZBACFZGZHBCIJGZBDRZCFZGZDCKZ
       LZUGUMUEAULGUGUMBACMUKUGDAULUIANUJUFBUIACSOPQTUEUHUMUAUGDBCUBUCUD $.
@@ -254197,9 +254229,10 @@ irreducible elements (see ~ df-irred ).  (Contributed by Mario Carneiro,
 
   ${
     $d F f $.  $d R f r s $.  $d S f r s $.  $d V f r s $.  $d W f r s $.
-    $( An isomorphism of rings is a homomorphism whose converse is also a
-       homomorphism .  (Contributed by AV, 22-Oct-2019.) $)
-    isrim0 $p |- ( ( R e. V /\ S e. W ) -> ( F e. ( R RingIso S )
+    $( Obsolete version of ~ isrim0 as of 12-Jan-2025.  (Contributed by AV,
+       22-Oct-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    isrim0OLD $p |- ( ( R e. V /\ S e. W ) -> ( F e. ( R RingIso S )
                  <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) ) ) $=
       ( vf vr vs wcel wa crs co cv ccnv crh crab cvv wceq a1i adantl cmpo rabex
       df-rngiso oveq12 ancoms eleq2d rabeqbidv adantr ovmpod cnveq eleq1d elrab
@@ -254214,6 +254247,20 @@ irreducible elements (see ~ df-irred ).  (Contributed by Mario Carneiro,
     rimrcl $p |- ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) ) $=
       ( vr vs vf cvv cv ccnv crh co wcel crab crs df-rngiso elmpocl ) DEGGFHIEH
       ZDHZJKLFRQJKMABNCFEDOP $.
+
+    $( A ring isomorphism is a homomorphism whose converse is also a
+       homomorphism.  Compare ~ isgim2 .  (Contributed by AV, 22-Oct-2019.)
+       Remove sethood antecedent.  (Revised by SN, 10-Jan-2025.) $)
+    isrim0 $p |- ( F e. ( R RingIso S ) <->
+                 ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) ) $=
+      ( vf vr vs crs co wcel cvv wa crh ccnv crg elexd cv crab wceq a1i oveq12
+      rimrcl rhmrcl1 rhmrcl2 jca adantr df-rngiso adantl ancoms rabeqbidv simpl
+      cmpo eleq2d simpr ovex rabex ovmpod cnveq eleq1d elrab bitrdi pm5.21nii )
+      CABGHZIZAJIZBJIZKZCABLHZIZCMZBALHZIZKZABCUAVHVFVKVHVDVEVHANABCUBOVHBNABCU
+      COUDUEVFVCCDPZMZVJIZDVGQZIVLVFVBVPCVFEFABJJVNFPZEPZLHZIZDVRVQLHZQZVPGJGEF
+      JJWBUKRVFDFEUFSVFVRARZVQBRZKZKZVTVODWAVGWEWAVGRVFVRAVQBLTUGWFVSVJVNWEVSVJ
+      RZVFWDWCWGVQBVRALTUHUGULUIVDVEUJVDVEUMVPJIVFVODVGABLUNUOSUPULVOVKDCVGVMCR
+      VNVIVJVMCUQURUSUTVA $.
   $}
 
   $( A ring homomorphism is an additive group homomorphism.  (Contributed by
@@ -254325,32 +254372,45 @@ irreducible elements (see ~ df-irred ).  (Contributed by Mario Carneiro,
       ABCDEFGVCSVDWHBAVKVLBAVKVBVIBADCVKGFVCVEVDABEVFVAVH $.
 
     $( An isomorphism of rings is a bijective homomorphism.  (Contributed by
-       AV, 22-Oct-2019.) $)
-    isrim $p |- ( ( R e. V /\ S e. W ) -> ( F e. ( R RingIso S )
+       AV, 22-Oct-2019.)  Remove sethood antecedent.  (Revised by SN,
+       12-Jan-2025.) $)
+    isrim $p |- ( F e. ( R RingIso S )
+            <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) ) $=
+      ( crs co wcel crh ccnv wa wf1o isrim0 rhmf1o bicomd pm5.32i bitri ) ECDHI
+      JECDKIJZELDCKIJZMTABENZMCDEOTUAUBTUBUAABCDEFGPQRS $.
+
+    $( Obsolete version of ~ isrim as of 12-Jan-2025.  (Contributed by AV,
+       22-Oct-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    isrimOLD $p |- ( ( R e. V /\ S e. W ) -> ( F e. ( R RingIso S )
                 <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) ) ) $=
-      ( wcel wa crs co crh ccnv wf1o isrim0 wb wi rhmf1o bicomd pm5.32d bitrd
-      a1i ) CFJDGJKZECDLMJECDNMJZEODCNMJZKUFABEPZKCDEFGQUEUFUGUHUFUGUHRSUEUFUHU
-      GABCDEHITUAUDUBUC $.
+      ( wcel wa crs co crh ccnv wf1o isrim0OLD wb wi rhmf1o bicomd a1i pm5.32d
+      bitrd ) CFJDGJKZECDLMJECDNMJZEODCNMJZKUFABEPZKCDEFGQUEUFUGUHUFUGUHRSUEUFU
+      HUGABCDEHITUAUBUCUD $.
 
     $( An isomorphism of rings is a bijection.  (Contributed by AV,
        22-Oct-2019.) $)
     rimf1o $p |- ( F e. ( R RingIso S ) -> F : B -1-1-onto-> C ) $=
-      ( cvv wcel wa crs co wf1o rimrcl crh isrim simpr syl6bi mpcom ) CHIDHIJZE
-      CDKLIZABEMZCDENTUAECDOLIZUBJUBABCDEHHFGPUCUBQRS $.
+      ( crs co wcel crh wf1o isrim simprbi ) ECDHIJECDKIJABELABCDEFGMN $.
 
-    $( An isomorphism of rings is a homomorphism.  (Contributed by AV,
-       22-Oct-2019.) $)
-    rimrhm $p |- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) ) $=
-      ( cvv wcel wa crs co crh rimrcl wf1o isrim simpl syl6bi mpcom ) CHIDHIJZE
-      CDKLIZECDMLIZCDENTUAUBABEOZJUBABCDEHHFGPUBUCQRS $.
+    $( Obsolete version of ~ rimrhm as of 12-Jan-2025.  (Contributed by AV,
+       22-Oct-2019.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    rimrhmOLD $p |- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) ) $=
+      ( crs co wcel crh wf1o isrim simplbi ) ECDHIJECDKIJABELABCDEFGMN $.
   $}
 
+  $( A ring isomorphism is a homomorphism.  Compare ~ gimghm .  (Contributed by
+     AV, 22-Oct-2019.)  Remove hypotheses.  (Revised by SN, 10-Jan-2025.) $)
+  rimrhm $p |- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) ) $=
+    ( crs co wcel crh ccnv isrim0 simplbi ) CABDEFCABGEFCHBAGEFABCIJ $.
+
   $( An isomorphism of rings is an isomorphism of their additive groups.
      (Contributed by AV, 24-Dec-2019.) $)
   rimgim $p |- ( F e. ( R RingIso S ) -> F e. ( R GrpIso S ) ) $=
-    ( crs co wcel cghm cbs cfv wf1o cgim crh eqid rimrhm rhmghm rimf1o sylanbrc
-    syl isgim ) CABDEFZCABGEFZAHIZBHIZCJCABKEFTCABLEFUAUBUCABCUBMZUCMZNABCORUBU
-    CABCUDUEPUBUCABCUDUESQ $.
+    ( crs co wcel cghm cbs cfv wf1o cgim crh rimrhm rhmghm eqid rimf1o sylanbrc
+    syl isgim ) CABDEFZCABGEFZAHIZBHIZCJCABKEFTCABLEFUAABCMABCNRUBUCABCUBOZUCOZ
+    PUBUCABCUDUESQ $.
 
   $( The composition of ring homomorphisms is a homomorphism.  (Contributed by
      Mario Carneiro, 12-Jun-2015.) $)
@@ -254520,11 +254580,10 @@ irreducible elements (see ~ df-irred ).  (Contributed by Mario Carneiro,
        JM's mathbox.  (Contributed by AV, 24-Dec-2019.) $)
     brric2 $p |- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring )
                                  /\ E. f f e. ( R RingIso S ) ) ) $=
-      ( cric wbr crs co c0 wne cv wcel wex crg wa brric cvv crh cmgp cfv eqid
-      n0 rimrcl ccnv isrim0 cghm cmhm isrhm simplbi adantr syl6bi mpcom exlimiv
-      pm4.71ri 3bitri ) ABDEABFGZHICJZUOKZCLZAMKBMKNZURNABOCUOUAURUSUQUSCAPKBPK
-      NZUQUSABUPUBUTUQUPABQGKZUPUCBAQGKZNUSABUPPPUDVAUSVBVAUSUPABUEGKUPARSZBRSZ
-      UFGKNABUPVCVDVCTVDTUGUHUIUJUKULUMUN $.
+      ( cric wbr crs co c0 wne cv wcel wex crg wa brric n0 crh cmgp cfv eqid
+      rimrhm cghm cmhm isrhm simplbi syl exlimiv pm4.71ri 3bitri ) ABDEABFGZHIC
+      JZUJKZCLZAMKBMKNZUMNABOCUJPUMUNULUNCULUKABQGKZUNABUKUAUOUNUKABUBGKUKARSZB
+      RSZUCGKNABUKUPUQUPTUQTUDUEUFUGUHUI $.
 
     $( If two rings are (ring) isomorphic, their additive groups are (group)
        isomorphic.  (Contributed by AV, 24-Dec-2019.) $)
@@ -282900,10 +282959,8 @@ represented as an element of (the base set of) ` ( ( 1 ... n ) Mat R ) ` .
     $( There is a ring isomorphism from a ring to the ring of matrices with
        dimension 1 over this ring.  (Contributed by AV, 22-Dec-2019.) $)
     mat1rngiso $p |- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingIso A ) ) $=
-      ( crg wcel wa crs co crh wf1o mat1rhm mat1f1o wb csn snfi matring sylancr
-      cfn simpl isrim syldan mpbir2and ) DOPZEIPZQZFDBRSPZFDBTSPZGCFUAZABCDEFGH
-      IJKLMNUBABCDEFGHIJKLMNUCUNUOBOPZUQURUSQUDUPEUEZUIPUNUTEUFUNUOUJBDVAKUGUHG
-      CDBFOOJLUKULUM $.
+      ( crg wcel wa crh co wf1o crs mat1rhm mat1f1o isrim sylanbrc ) DOPEIPQFDB
+      RSPGCFTFDBUASPABCDEFGHIJKLMNUBABCDEFGHIJKLMNUCGCDBFJLUDUE $.
   $}
 
   ${
@@ -283827,12 +283884,10 @@ matrix over (the ring) ` R ` .  (Contributed by AV, 18-Dec-2019.) $)
        29-Dec-2019.) $)
     scmatrngiso $p |- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring )
                         -> F e. ( R RingIso S ) ) $=
-      ( wcel crg cfv cfn c0 wne w3a crs crh wf1o scmatrhm 3adant2 scmatf1o wceq
-      co cbs scmatstrbas f1oeq3d mpbird wa simp3 csubrg c0g scmatsrng subrgring
-      wb eqid syl isrim 3imp3i2an mpbir2and ) JUARZJUBUCZDSRZUDZGDEUEULRZGDEUFU
-      LRZIEUMTZGUGZVIVKVNVJABCDEFGHIJKLMNOPQUHUIVLVPICGUGABCDFGHIJKLMNOPUJVLVOC
-      IGVIVKVOCUKVJBCDEJLPQUNUIUOUPVIVJVKVKESRZVMVNVPUQVCVIVJVKURVIVKUQCBUSTRVQ
-      BBUMTZDCIJDUTTZLVRVDKVSVDPVACBEQVBVEIVODEGSSKVOVDVFVGVH $.
+      ( wcel co wf1o cfn wne crg w3a crh cbs cfv scmatrhm 3adant2 scmatf1o wceq
+      c0 crs scmatstrbas f1oeq3d mpbird eqid isrim sylanbrc ) JUARZJULUBZDUCRZU
+      DZGDEUESRZIEUFUGZGTZGDEUMSRUTVBVDVAABCDEFGHIJKLMNOPQUHUIVCVFICGTABCDFGHIJ
+      KLMNOPUJVCVECIGUTVBVECUKVABCDEJLPQUNUIUOUPIVEDEGKVEUQURUS $.
   $}
 
   ${
@@ -289258,14 +289313,12 @@ whose entries are constant polynomials (or "scalar polynomials", see
        ring isomorphism.  (Contributed by AV, 19-Nov-2019.) $)
     m2cpmrngiso $p |- ( ( N e. Fin /\ R e. CRing )
                         -> T e. ( A RingIso U ) ) $=
-      ( wcel wa cfv crg vm cfn ccrg crs crh cbs wf1o m2cpmrhm crngring m2cpmf1o
-      co anim2i wss wceq cv eqid cpmatpmat 3expia ssrdv ressbas2 eqcomd f1oeq3d
-      syl mpbird cgrp wb matring csubg cpmatsubgpmat subggrp 3syl isrim syl2anc
-      mpbir2and ) IUBQZDUCQZRZFAGUDUKQZFAGUEUKQZHGUFSZFUGZAHBCDEFGIJKLMNOPUHVQV
-      ODTQZRZWAVPWBVODUIULZWCWAHEFUGADEFHIJKLMUJWCVTEHFWCEVTWCEBUFSZUMEVTUNWCUA
-      EWEVOWBUAUOZEQWFWEQWEBCDEWFITJNOWEUPZUQURUSEWEGBPWGUTVCVAVBVDVCVQATQZGVEQ
-      ZVRVSWARVFVQWCWHWDADILVGVCVQWCEBVHSQWIWDBCDEIJNOVIEBGPVJVKHVTAGFTVEMVTUPV
-      LVMVN $.
+      ( vm wcel wa co cfn ccrg crh cbs cfv wf1o m2cpmrhm crngring m2cpmf1o wceq
+      crs crg wss cv eqid cpmatpmat 3expia ssrdv ressbas2 eqcomd f1oeq3d mpbird
+      syl sylan2 isrim sylanbrc ) IUARZDUBRZSFAGUCTRHGUDUEZFUFZFAGUKTRAHBCDEFGI
+      JKLMNOPUGVHVGDULRZVJDUHVGVKSZVJHEFUFADEFHIJKLMUIVLVIEHFVLEVIVLEBUDUEZUMEV
+      IUJVLQEVMVGVKQUNZERVNVMRVMBCDEVNIULJNOVMUOZUPUQUREVMGBPVOUSVCUTVAVBVDHVIA
+      GFMVIUOVEVF $.
   $}
 
   ${
@@ -291221,11 +291274,9 @@ over matrices (over the same ring).  (Contributed by AV, 5-Dec-2019.) $)
     $( The transformation of polynomial matrices into polynomials over matrices
        is a ring isomorphism.  (Contributed by AV, 22-Oct-2019.) $)
     pm2mprngiso $p |- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingIso Q ) ) $=
-      ( cfn wcel crg wa co cbs cfv eqid crs crh wf1o pm2mprhm cmgp cmg pm2mpf1o
-      cvsca cv1 wb pmatring matring ply1ring syl isrim syl2anc mpbir2and ) GMNE
-      ONPZFBDUAQNZFBDUBQNZBRSZDRSZFUCZABCDEFGHIJKLUDAVABCDEFDUESUFSZDUHSZVBGAUI
-      SZHIVATZVETVDTVFTJKVBTZLUGURBONDONZUSUTVCPUJBCEGHIUKURAONVIAEGJULDAKUMUNV
-      AVBBDFOOVGVHUOUPUQ $.
+      ( cfn wcel crg wa co cbs cfv eqid crh wf1o crs pm2mprhm cmgp cmg pm2mpf1o
+      cvsca cv1 isrim sylanbrc ) GMNEONPFBDUAQNBRSZDRSZFUBFBDUCQNABCDEFGHIJKLUD
+      AULBCDEFDUESUFSZDUHSZUMGAUISZHIULTZUOTUNTUPTJKUMTZLUGULUMBDFUQURUJUK $.
   $}
 
   ${
@@ -317239,13 +317290,11 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
 
   ${
     $d x U $.  $d x X $.
-    $( First direction for ~ ustbas .  (Contributed by Thierry Arnoux,
-       16-Nov-2017.) $)
-    elrnust $p |- ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn ) $=
-      ( vx cust cfv wcel cv cdm wrex crn cuni elfvdm wceq eleq2d rspcev mpancom
-      fveq2 cvv wfn wfun wb ustfn fnfun elunirn mp2b sylibr ) ABDEZFZACGZDEZFZC
-      DHZIZADJKFZBULFUHUMABDLUKUHCBULUIBMUJUGAUIBDQNOPDRSDTUNUMUAUBRDUCCADUDUEU
-      F $.
+    $( Obsolete version of ~ elfvunirn as of 12-Jan-2025.  (Contributed by
+       Thierry Arnoux, 16-Nov-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    elrnustOLD $p |- ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn ) $=
+      ( cust elfvunirn ) BACD $.
   $}
 
   ${
@@ -317279,9 +317328,9 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
        Arnoux, 16-Nov-2017.) $)
     ustbas $p |- ( U e. U. ran UnifOn <-> U e. ( UnifOn ` X ) ) $=
       ( vx cust crn cuni wcel cfv cv cdm wrex cvv wfun ustfn fnfun elunirn mp2b
-      wfn wb ustbas2 eqtr4di fveq2d eleq2d ibi rexlimivw sylbi elrnust impbii )
-      AEFGHZABEIZHZUJADJZEIZHZDEKZLZULEMSENUJUQTOMEPDAEQRUOULDUPUOULUOUNUKAUOUM
-      BEUOUMAGKBAUMUACUBUCUDUEUFUGABUHUI $.
+      wfn wb ustbas2 eqtr4di fveq2d eleq2d ibi rexlimivw sylbi elfvunirn impbii
+      ) AEFGHZABEIZHZUJADJZEIZHZDEKZLZULEMSENUJUQTOMEPDAEQRUOULDUPUOULUOUNUKAUO
+      UMBEUOUMAGKBAUMUACUBUCUDUEUFUGBAEUHUI $.
   $}
 
   $( Lemma for ~ ustuqtop .  (Contributed by Thierry Arnoux, 5-Dec-2017.) $)
@@ -317381,10 +317430,10 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
       A. x e. a E. v e. U ( v " { x } ) C_ a } ) $=
       ( vu cust cfv wcel cv csn cima wrex wral cuni cdm cpw crab cvv wceq cutop
       wss crn df-utop wa simpr unieqd dmeqd ustbas2 adantr eqtr4d pweqd rexeqdv
-      ralbidv rabeqbidv elrnust elfvex pwexg rabexg 3syl fvmptd2 ) CDGHIZFCBJAJ
-      KLEJZUBZBFJZMZAVCNZEVEOZPZQZRVDBCMZAVCNZEDQZRZGUCOUASABFEUDVBVECTZUEZVGVL
-      EVJVMVPVIDVPVICOZPZDVPVHVQVPVECVBVOUFZUGUHVBDVRTVOCDUIUJUKULVPVFVKAVCVPVD
-      BVECVSUMUNUOCDUPVBDSIVMSIVNSICDGUQDSURVLEVMSUSUTVA $.
+      ralbidv rabeqbidv elfvunirn elfvex pwexg rabexg 3syl fvmptd2 ) CDGHIZFCBJ
+      AJKLEJZUBZBFJZMZAVCNZEVEOZPZQZRVDBCMZAVCNZEDQZRZGUCOUASABFEUDVBVECTZUEZVG
+      VLEVJVMVPVIDVPVICOZPZDVPVHVQVPVECVBVOUFZUGUHVBDVRTVOCDUIUJUKULVPVFVKAVCVP
+      VDBVECVSUMUNUODCGUPVBDSIVMSIVNSICDGUQDSURVLEVMSUSUTVA $.
   $}
 
   ${
@@ -318001,9 +318050,9 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
         sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) $=
       ( vu cust cfv wcel cnx cbs cv cuni cdm cop cunif cpr cutop csts co opeq2d
       cts crn ctus cvv df-tus wceq wa simpr unieqd dmeqd preq12d fveq2d oveq12d
-      elrnust ovexd fvmptd2 ) ABDEFZCAGHEZCIZJZKZLZGMEZUQLZNZGSEZUQOEZLZPQUPAJZ
-      KZLZVAALZNZVDAOEZLZPQDTJUAUBCUCUOUQAUDZUEZVCVKVFVMPVOUTVIVBVJVOUSVHUPVOUR
-      VGVOUQAUOVNUFZUGUHRVOUQAVAVPRUIVOVEVLVDVOUQAOVPUJRUKABULUOVKVMPUMUN $.
+      elfvunirn ovexd fvmptd2 ) ABDEFZCAGHEZCIZJZKZLZGMEZUQLZNZGSEZUQOEZLZPQUPA
+      JZKZLZVAALZNZVDAOEZLZPQDTJUAUBCUCUOUQAUDZUEZVCVKVFVMPVOUTVIVBVJVOUSVHUPVO
+      URVGVOUQAUOVNUFZUGUHRVOUQAVAVPRUIVOVEVLVDVOUQAOVPUJRUKBADULUOVKVMPUMUN $.
 
     tuslem.k $e |- K = ( toUnifSp ` U ) $.
     $( Lemma for ~ tusbas , ~ tusunif , and ~ tustopn .  (Contributed by
@@ -318137,17 +318186,17 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
     ucnval $p |- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) )
       -> ( U uCn V ) = { f e. ( Y ^m X ) | A. s e. V E. r e. U
             A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } ) $=
-      ( vu vv cfv wcel co cv cuni cdm wral cmap wceq cust wa cucn wbr wrex crab
-      wi crn cvv elrnust adantr adantl ovex rabex a1i simpr dmeqd simpl oveq12d
-      unieqd raleqdv raleqbidv rexeqbidv df-ucn ovmpoga syl3anc ustbas2 rexbidv
-      rabeqbidv oveqan12rd ralbidv eqtr4d ) CFUALMZEGUALMZUBZCEUCNZAOZBOZIOUDVQ
-      DOZLVRVSLHOUDUGZBCPZQZRZAWBRZICUEZHERZDEPZQZWBSNZUFZVTBFRZAFRZICUEZHERZDG
-      FSNZUFVOCUAUHPZMZEWPMZWJUIMZVPWJTVMWQVNCFUJUKVNWRVMEGUJULWSVOWFDWIWHWBSUM
-      UNUOJKCEWPWPVTBJOZPZQZRZAXBRZIWTUEZHKOZRZDXFPZQZXBSNZUFWJUCUIWTCTZXFETZUB
-      ZXGWFDXJWIXMXIWHXBWBSXMXHWGXMXFEXKXLUPZUTUQXMXAWAXMWTCXKXLURZUTUQZUSXMXEW
-      EHXFEXNXMXDWDIWTCXOXMXCWCAXBWBXPXMVTBXBWBXPVAVBVCVBVIABKJDHIVDVEVFVOWNWFD
-      WOWIVNVMGWHFWBSEGVGCFVGZVJVOWMWEHEVOWLWDICVOWKWCAFWBVMFWBTVNXQUKZVOVTBFWB
-      XRVAVBVHVKVIVL $.
+      ( vu cust cfv wcel co cv cuni cdm wral cmap wceq vv wa cucn wbr wrex crab
+      crn cvv elfvunirn adantr adantl ovex rabex a1i simpr unieqd dmeqd oveq12d
+      wi simpl raleqdv raleqbidv rexeqbidv rabeqbidv ovmpoga syl3anc oveqan12rd
+      df-ucn ustbas2 rexbidv ralbidv eqtr4d ) CFKLMZEGKLMZUBZCEUCNZAOZBOZIOUDVQ
+      DOZLVRVSLHOUDUSZBCPZQZRZAWBRZICUEZHERZDEPZQZWBSNZUFZVTBFRZAFRZICUEZHERZDG
+      FSNZUFVOCKUGPZMZEWPMZWJUHMZVPWJTVMWQVNFCKUIUJVNWRVMGEKUIUKWSVOWFDWIWHWBSU
+      LUMUNJUACEWPWPVTBJOZPZQZRZAXBRZIWTUEZHUAOZRZDXFPZQZXBSNZUFWJUCUHWTCTZXFET
+      ZUBZXGWFDXJWIXMXIWHXBWBSXMXHWGXMXFEXKXLUOZUPUQXMXAWAXMWTCXKXLUTZUPUQZURXM
+      XEWEHXFEXNXMXDWDIWTCXOXMXCWCAXBWBXPXMVTBXBWBXPVAVBVCVBVDABUAJDHIVHVEVFVOW
+      NWFDWOWIVNVMGWHFWBSEGVICFVIZVGVOWMWEHEVOWLWDICVOWKWCAFWBVMFWBTVNXQUJZVOVT
+      BFWBXRVAVBVJVKVDVL $.
   $}
 
   ${
@@ -318390,12 +318439,12 @@ unit group (that is, the nonzero numbers) to the field.  (Contributed
     iscfilu $p |- ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <->
       ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) ) $=
       ( vf vu cust cfv wcel ccfilu cuni cdm cfbas cv wrex wral wa crab wceq cxp
-      wss crn elrnust unieq dmeqd raleq rabeqbidv df-cfilu fvex rabex fvmpt syl
-      fveq2d eleq2d rexeq ralbidv elrab bitrdi ustbas2 anbi1d bitr4d ) BDHIJZCB
-      KIZJZCBLZMZNIZJZEOZVJUAAOUBZECPZABQZRZCDNIZJZVMRVCVECVKEFOZPZABQZFVHSZJVN
-      VCVDVTCVCBHUCLZJVDVTTBDUDGBVRAGOZQZFWBLZMZNIZSVTWAKWBBTZWCVSFWFVHWGWEVGNW
-      GWDVFWBBUEUFUNVRAWBBUGUHAGFEUIVSFVHVGNUJUKULUMUOVSVMFCVHVQCTVRVLABVKEVQCU
-      PUQURUSVCVPVIVMVCVOVHCVCDVGNBDUTUNUOVAVB $.
+      wss crn elfvunirn unieq dmeqd fveq2d raleq rabeqbidv df-cfilu rabex fvmpt
+      fvex syl eleq2d rexeq ralbidv elrab bitrdi ustbas2 anbi1d bitr4d ) BDHIJZ
+      CBKIZJZCBLZMZNIZJZEOZVJUAAOUBZECPZABQZRZCDNIZJZVMRVCVECVKEFOZPZABQZFVHSZJ
+      VNVCVDVTCVCBHUCLZJVDVTTDBHUDGBVRAGOZQZFWBLZMZNIZSVTWAKWBBTZWCVSFWFVHWGWEV
+      GNWGWDVFWBBUEUFUGVRAWBBUHUIAGFEUJVSFVHVGNUMUKULUNUOVSVMFCVHVQCTVRVLABVKEV
+      QCUPUQURUSVCVPVIVMVCVOVHCVCDVGNBDUTUGUOVAVB $.
   $}
 
   ${
@@ -322600,17 +322649,12 @@ S C_ ( P ( ball ` D ) T ) ) $=
        11-Feb-2018.) $)
     metuval $p |- ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X )
       filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) ) $=
-      ( vd vx vy vz vu vw vv cpsmet wcel cv cdm cxp crp co crn cfg wceq cfv cc0
-      ccnv cico cima cmpt cmetu cvv df-metu simpr dmeqd psmetdmdm adantr eqtr4d
-      cuni wa sqxpeqd simplr cnveqd imaeq1d mpteq2dva rneqd oveq12d wrex elfvdm
-      fveq2 eleq2d rspcev mpancom wfun cxad cle wbr wral cxr cmap crab df-psmet
-      wb funmpt2 elunirn ax-mp sylibr ovexd fvmptd2 ) ABKUAZLZDADMZNZNZWJOZCPWH
-      UCZUBCMZUDQZUEZUFZRZSQBBOZCPAUCZWNUEZUFZRZSQKRUOZUGUHCDUIWGWHATZUPZWKWRWQ
-      XBSXEWJBXEWJANZNZBXEWIXFXEWHAWGXDUJUKUKWGBXGTXDABULUMUNUQXEWPXAXECPWOWTXE
-      WMPLZUPZWLWSWNXIWHAWGXDXHURUSUTVAVBVCWGAEMZKUAZLZEKNZVDZAXCLZBXMLWGXNABKV
-      EXLWGEBXMXJBTXKWFAXJBKVFVGVHVIKVJXOXNVSFUHGMZXPHMZQUBTXPIMZXQQJMZXPXQQXSX
-      RXQQVKQVLVMJFMZVNIXTVNUPGXTVNHVOXTXTOVPQVQKFGIJHVRVTEAKWAWBWCWGWRXBSWDWE
-      $.
+      ( vd cpsmet cfv wcel cv cdm cxp crp ccnv co cima cmpt crn cfg wceq dmeqd
+      wa cc0 cico cuni cmetu cvv df-metu psmetdmdm adantr eqtr4d sqxpeqd simplr
+      simpr cnveqd imaeq1d mpteq2dva rneqd oveq12d elfvunirn ovexd fvmptd2 ) AB
+      EFGZDADHZIZIZVDJZCKVBLZUACHZUBMZNZOZPZQMBBJZCKALZVHNZOZPZQMEPUCUDUECDUFVA
+      VBARZTZVEVLVKVPQVRVDBVRVDAIZIZBVRVCVSVRVBAVAVQULSSVABVTRVQABUGUHUIUJVRVJV
+      OVRCKVIVNVRVGKGZTZVFVMVHWBVBAVAVQWAUKUMUNUOUPUQBAEURVAVLVPQUSUT $.
   $}
 
   ${
@@ -494036,17 +494080,13 @@ closed sets (see for example ~ zarcls0 for the definition of ` V ` ).
        Arnoux, 7-Feb-2018.) $)
     metidval $p |- ( D e. ( PsMet ` X ) -> ( ~Met ` D ) =
       { <. x , y >. | ( ( x e. X /\ y e. X ) /\ ( x D y ) = 0 ) } ) $=
-      ( vd vz vw cpsmet cfv wcel cv cdm wa co cc0 wceq copab cvv eleq2d wral wb
-      crn cuni cmetid cmpt df-metid simpr dmeqd psmetdmdm adantr eqtr4d anbi12d
-      a1i oveqd eqeq1d opabbidv wrex elfvdm fveq2 mpancom wfun cxad cle wbr cxr
-      rspcev cxp cmap df-psmet funmpt2 elunirn ax-mp sylibr wss opabssxp elfvex
-      crab xpexd ssexg sylancr fvmptd ) CDHIZJZECAKZEKZLZLZJZBKZWGJZMZWDWIWENZO
-      PZMZABQZWDDJZWIDJZMZWDWICNZOPZMZABQZHUBUCZUDRUDEXCWOUEPWCABEUFUMWCWECPZMZ
-      WNXAABXEWKWRWMWTXEWHWPWJWQXEWGDWDXEWGCLZLZDXEWFXFXEWECWCXDUGZUHUHWCDXGPXD
-      CDUIUJUKZSXEWGDWIXISULXEWLWSOXEWECWDWIXHUNUOULUPWCCWDHIZJZAHLZUQZCXCJZDXL
-      JWCXMCDHURXKWCADXLWDDPXJWBCWDDHUSSVFUTHVAXNXMUAARWIWIWENOPWIFKZWENGKZWIWE
-      NXPXOWENVBNVCVDGWDTFWDTMBWDTEVEWDWDVGVHNVQHABFGEVIVJACHVKVLVMWCXBDDVGZVNX
-      QRJXBRJWTABDDVOWCDDRRCDHVPZXRVRXBXQRVSVTWA $.
+      ( vd cpsmet cfv wcel cv cdm wa co cc0 wceq copab crn dmeqd eleq2d anbi12d
+      cvv cuni cmetid df-metid simpr psmetdmdm adantr eqtr4d opabbidv elfvunirn
+      oveqd eqeq1d cxp wss opabssxp elfvex xpexd ssexg sylancr fvmptd2 ) CDFGHZ
+      ECAIZEIZJZJZHZBIZVDHZKZVAVFVBLZMNZKZABOVADHZVFDHZKZVAVFCLZMNZKZABOZFPUAUB
+      TABEUCUTVBCNZKZVKVQABVTVHVNVJVPVTVEVLVGVMVTVDDVAVTVDCJZJZDVTVCWAVTVBCUTVS
+      UDZQQUTDWBNVSCDUEUFUGZRVTVDDVFWDRSVTVIVOMVTVBCVAVFWCUJUKSUHDCFUIUTVRDDULZ
+      UMWETHVRTHVPABDDUNUTDDTTCDFUOZWFUPVRWETUQURUS $.
 
     $( As a relation, the metric identification is a subset of a Cartesian
        product.  (Contributed by Thierry Arnoux, 7-Feb-2018.) $)
@@ -494129,21 +494169,17 @@ closed sets (see for example ~ zarcls0 for the definition of ` V ` ).
     pstmval $p |- ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) =
       ( a e. ( X /. .~ ) , b e. ( X /. .~ )
       |-> U. { z | E. x e. a E. y e. b z = ( x D y ) } ) ) $=
-      ( vd vc cpsmet cfv wcel cv cdm co wceq wrex cvv cmetid cqs cab cuni cpstm
-      cmpo crn cmpt df-pstm a1i psmetdmdm adantr dmeq dmeqd adantl eqtr4d qseq1
-      wa syl fveq2 eqtr4id qseq2 eqtr2d mpoeq12 syl2anc w3a simp1r oveqd eqeq2d
-      2rexbidv abbidv unieqd mpoeq3dva elfvdm eleq2d rspcev mpancom wfun wb cc0
-      eqtrd cxad cle wbr wral cxr cxp cmap crab df-psmet funmpt2 elunirn sylibr
-      ax-mp elfvex qsexg mpoexga fvmptd ) DFLMZNZJDGHJOZPZPZXAUAMZUBZXECOZAOZBO
-      ZXAQZRZBHOZSAGOZSZCUCZUDZUFZGHFEUBZXQXFXGXHDQZRZBXKSAXLSZCUCZUDZUFZLUGUDZ
-      UETUEJYDXPUHRWTABCGHJUIUJWTXADRZURZXPGHXQXQXOUFZYCYFXEXQRZYHXPYGRYFXQXCEU
-      BZXEYFFXCRXQYIRYFFDPZPZXCWTFYKRYEDFUKULYEXCYKRWTYEXBYJXADUMUNUOUPFXCEUQUS
-      YEYIXERZWTYEEXDRYLYEEDUAMXDIXADUAUTVAEXDXCVBUSUOVCZYMGHXEXEXQXQXOVDVEYFGH
-      XQXQXOYBYFXLXQNZXKXQNZVFZXNYAYPXMXTCYPXJXSABXLXKYPXIXRXFYPXADXGXHWTYEYNYO
-      VGVHVIVJVKVLVMWAWTDXGLMZNZALPZSZDYDNZFYSNWTYTDFLVNYRWTAFYSXGFRYQWSDXGFLUT
-      VOVPVQLVRUUAYTVSATXLXLXAQVTRXLXKXAQKOZXLXAQUUBXKXAQWBQWCWDKXGWEHXGWEURGXG
-      WEJWFXGXGWGWHQWILAGHKJWJWKADLWLWNWMWTXQTNZUUCYCTNWTFTNUUCDFLWOFETWPUSZUUD
-      GHXQXQYBTTWQVEWR $.
+      ( vd cpsmet cfv wcel cv cdm cmetid cqs wceq wrex cvv co cab cuni cmpo crn
+      cpstm df-pstm psmetdmdm adantr dmeq dmeqd adantl eqtr4d qseq1 syl eqtr4id
+      fveq2 qseq2d eqtr2d mpoeq12 syl2anc w3a simp1r oveqd eqeq2d abbidv unieqd
+      wa 2rexbidv mpoeq3dva eqtrd elfvunirn elfvex qsexg mpoexga fvmptd2 ) DFKL
+      MZJDGHJNZOZOZVRPLZQZWBCNZANZBNZVRUAZRZBHNZSAGNZSZCUBZUCZUDZGHFEQZWNWCWDWE
+      DUAZRZBWHSAWISZCUBZUCZUDZKUEUCUFTABCGHJUGVQVRDRZVHZWMGHWNWNWLUDZWTXBWBWNR
+      ZXDWMXCRXBWNVTEQZWBXBFVTRWNXERXBFDOZOZVTVQFXGRXADFUHUIXAVTXGRVQXAVSXFVRDU
+      JUKULUMFVTEUNUOXAXEWBRVQXAEWAVTXAEDPLWAIVRDPUQUPURULUSZXHGHWBWBWNWNWLUTVA
+      XBGHWNWNWLWSXBWIWNMZWHWNMZVBZWKWRXKWJWQCXKWGWPABWIWHXKWFWOWCXKVRDWDWEVQXA
+      XIXJVCVDVEVIVFVGVJVKFDKVLVQWNTMZXLWTTMVQFTMXLDFKVMFETVNUOZXMGHWNWNWSTTVOV
+      AVP $.
 
     $d a b e f z .~ $.  $d a b e f x y z A $.  $d a b e f x y z B $.
     $d e f z D $.  $d e f z X $.
@@ -500344,14 +500380,12 @@ strict in the case where the sets B(x) overlap.  (Contributed by Thierry
 
     $( The base set of a measure is its domain.  (Contributed by Thierry
        Arnoux, 25-Dec-2016.) $)
-    measbasedom $p |- ( M e. U. ran measures
-                                             <-> M e. ( measures ` dom M ) ) $=
-      ( vx vy vs vm cmeas crn cuni wcel cfv cc0 wf c0 wceq cv cesum wi cpw wral
-      w3a cdm cpnf cicc co com wbr wdisj wa csiga isrnmeas simprd dmmeas ismeas
-      cdom wb syl mpbird wfun cab df-meas funmpt2 elunirn2 mpan impbii ) AFGHIZ
-      AAUAZFJIZVEVGVFKUBUCUDZALMAJKNBOZUEUNUFCVICOZUGUHZVIHZAJVIVJAJCPNQBVFRSTZ
-      VEVFUIGHZIZVMBCAUJUKVEVOVGVMUOAULBCVFAUMUPUQFURVGVEDVNDOZVHEOZLMVQJKNVKVL
-      VQJVIVJVQJCPNQBVPRSTEUSFBCEDUTVAVFAFVBVCVD $.
+    measbasedom $p |- ( M e. U. ran measures <-> M e. ( measures ` dom M ) ) $=
+      ( vx vy cmeas crn cuni wcel cdm cfv cc0 cpnf cicc co wf wceq com cdom wbr
+      c0 cv wdisj wa cesum cpw wral w3a csiga isrnmeas simprd dmmeas ismeas syl
+      wi wb mpbird elfvunirn impbii ) ADEFGZAAHZDIGZURUTUSJKLMANSAIJOBTZPQRCVAC
+      TZUAUBVAFAIVAVBAICUCOUMBUSUDUEUFZURUSUGEFGZVCBCAUHUIURVDUTVCUNAUJBCUSAUKU
+      LUOUSADUPUQ $.
   $}
 
   ${
@@ -501331,16 +501365,11 @@ strict in the case where the sets B(x) overlap.  (Contributed by Thierry
       mpbid syl ) ADCIZBIZJKLZUFUEDMAUGDNHOPBLHCQZADBCRKLUGUHSGAHBCDEFTUCUADUEU
       FUBUD $.
 
-    $( The predicate to be a measurable function.  (Contributed by Thierry
-       Arnoux, 30-Jan-2017.) $)
-    isanmbfm $p |- ( ph -> F e. U. ran MblFnM ) $=
-      ( vt vs vx cv cuni cmap co wcel wral wa crn wrex cmbfm csiga ismbfm mpbid
-      ccnv cima wceq unieq oveq2d eleq2d ralbidv anbi12d oveq1d rspc2ev syl3anc
-      eleq2 raleq elunirnmbfm sylibr ) ADHKZLZIKZLZMNZOZDUDJKUEZVAOZJUSPZQZHUAR
-      LZSIVISZDTRLOABVIOCVIODCLZBLZMNZOZVEBOZJCPZQZVJEFADBCTNOVQGAJBCDEFUBUCVHV
-      QDUTVLMNZOZVOJUSPZQIHBCVIVIVABUFZVDVSVGVTWAVCVRDWAVBVLUTMVABUGUHUIWAVFVOJ
-      USVABVEUOUJUKUSCUFZVSVNVTVPWBVRVMDWBUTVKVLMUSCUGULUIVOJUSCUPUKUMUNJHDIUQU
-      R $.
+    $( Obsolete version of ~ isanmbfm as of 13-Jan-2025.  (Contributed by
+       Thierry Arnoux, 30-Jan-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    isanmbfmOLD $p |- ( ph -> F e. U. ran MblFnM ) $=
+      ( cmbfm co crn cuni ovssunirn sselid ) ABCHIHJKDHBCLGM $.
 
     $d x A $.
     mbfmcnvima.4 $e |- ( ph -> A e. T ) $.
@@ -501353,15 +501382,32 @@ strict in the case where the sets B(x) overlap.  (Contributed by Thierry
   $}
 
   ${
-    mbfmbfm.1 $e |- ( ph -> M e. U. ran measures ) $.
-    mbfmbfm.2 $e |- ( ph -> J e. Top ) $.
-    mbfmbfm.3 $e |- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) ) $.
+    isanmbfm.1 $e |- ( ph -> F e. ( S MblFnM T ) ) $.
+    $( The predicate to be a measurable function.  (Contributed by Thierry
+       Arnoux, 30-Jan-2017.)  Remove hypotheses.  (Revised by SN,
+       13-Jan-2025.) $)
+    isanmbfm $p |- ( ph -> F e. U. ran MblFnM ) $=
+      ( cmbfm co crn cuni ovssunirn sselid ) ABCFGFHIDFBCJEK $.
+  $}
+
+  ${
+    mbfmbfmOLD.1 $e |- ( ph -> M e. U. ran measures ) $.
+    mbfmbfmOLD.2 $e |- ( ph -> J e. Top ) $.
+    mbfmbfmOLD.3 $e |- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) ) $.
     $( A measurable function to a Borel Set is measurable.  (Contributed by
-       Thierry Arnoux, 24-Jan-2017.) $)
+       Thierry Arnoux, 24-Jan-2017.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    mbfmbfmOLD $p |- ( ph -> F e. U. ran MblFnM ) $=
+      ( cdm csigagen cfv isanmbfm ) ADHCIJBGK $.
+  $}
+
+  ${
+    mbfmbfm.1 $e |- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) ) $.
+    $( A measurable function to a Borel Set is measurable.  (Contributed by
+       Thierry Arnoux, 24-Jan-2017.)  Remove hypotheses.  (Revised by SN,
+       13-Jan-2025.) $)
     mbfmbfm $p |- ( ph -> F e. U. ran MblFnM ) $=
-      ( cdm csigagen cfv cmeas cuni wcel csiga measbasedom biimpi measbase 3syl
-      crn ctop sgsiga isanmbfm ) ADHZCIJBADKSLMZDUCKJMZUCNSLMEUDUEDOPUCDQRACTFU
-      AGUB $.
+      ( cdm csigagen cfv isanmbfm ) ADFCGHBEI $.
   $}
 
   ${
@@ -501666,18 +501712,18 @@ strict in the case where the sets B(x) overlap.  (Contributed by Thierry
       u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR ) $=
       ( vz cr cv cpnf cico co cxp cmpt cuni wss wcel pnfxr syl ovex reex cfv wa
       xpex crn cun unissb wo elun cpw eqid rnmptss cxr icossre mpan2 xpss1 elpw
-      sylibr mprg sseli elpwid xpss2 jaoi mprgbir wfun c1st funmpt cvv c2nd clt
-      sylbi wbr rexr a1i ltpnf lbico1 syl3anc anim1i anim2i elxp7 3imtr4i xp1st
-      wceq oveq1 xpeq1d fvmpt eleqtrrd elunirn2 sylancr ssriv ssun3 ax-mp uniun
-      sseqtrri eqssi ) ADAEZFGHZDIZJZUAZBDDBEZFGHZIZJZUAZUBZKZDDIZXCXDLCEZXDLZC
-      XBCXBXDUCXEXBMXEWPMZXEXAMZUDXFXEWPXAUEXGXFXHXGXEXDWPXDUFZXEWNXIMZWPXILADA
-      DWNXIWOWOUGZUHWLDMZWNXDLZXJXLWMDLZXMXLFUIMZXNNWLFUJUKWMDDULOWNXDWMDWLFGPQ
-      TUMUNUOUPUQXHXEXDXAXIXEWSXIMZXAXILBDBDWSXIWTWTUGUHWQDMZWSXDLZXPXQWRDLZXRX
-      QXOXSNWQFUJUKWRDDUROWSXDDWRQWQFGPTUMUNUOUPUQUSVGUTXDWPKZXAKZUBZXCXDXTLXDY
-      BLCXDXTXEXDMZWOVAXEXEVBRZWORZMXEXTMADWNVCYCXEYDFGHZDIZYEXEVDVDIMZYDDMZXEV
-      ERDMZSZSYHYDYFMZYJSZSYCXEYGMYKYMYHYIYLYJYIYDUIMXOYDFVFVHYLYDVIXOYINVJYDVK
-      YDFVLVMVNVOXEDDVPXEYFDVPVQYCYIYEYGVSXEDDVRAYDWNYGDWOWLYDVSWMYFDWLYDFGVTWA
-      XKYFDYDFGPQTWBOWCYDXEWOWDWEWFXDXTYAWGWHWPXAWIWJWK $.
+      sylibr mprg sseli xpss2 jaoi sylbi mprgbir c1st cvv c2nd clt wbr rexr a1i
+      elpwid ltpnf lbico1 syl3anc anim1i anim2i elxp7 3imtr4i wceq xp1st xpeq1d
+      oveq1 fvmpt eleqtrrd elfvunirn ssriv ssun3 ax-mp uniun sseqtrri eqssi ) A
+      DAEZFGHZDIZJZUAZBDDBEZFGHZIZJZUAZUBZKZDDIZWTXALCEZXALZCWSCWSXAUCXBWSMXBWM
+      MZXBWRMZUDXCXBWMWRUEXDXCXEXDXBXAWMXAUFZXBWKXFMZWMXFLADADWKXFWLWLUGZUHWIDM
+      ZWKXALZXGXIWJDLZXJXIFUIMZXKNWIFUJUKWJDDULOWKXAWJDWIFGPQTUMUNUOUPVHXEXBXAW
+      RXFXBWPXFMZWRXFLBDBDWPXFWQWQUGUHWNDMZWPXALZXMXNWODLZXOXNXLXPNWNFUJUKWODDU
+      QOWPXADWOQWNFGPTUMUNUOUPVHURUSUTXAWMKZWRKZUBZWTXAXQLXAXSLCXAXQXBXAMZXBXBV
+      ARZWLRZMXBXQMXTXBYAFGHZDIZYBXBVBVBIMZYADMZXBVCRDMZSZSYEYAYCMZYGSZSXTXBYDM
+      YHYJYEYFYIYGYFYAUIMXLYAFVDVEYIYAVFXLYFNVGYAVIYAFVJVKVLVMXBDDVNXBYCDVNVOXT
+      YFYBYDVPXBDDVQAYAWKYDDWLWIYAVPWJYCDWIYAFGVSVRXHYCDYAFGPQTVTOWAYAXBWLWBOWC
+      XAXQXRWDWEWMWRWFWGWH $.
   $}
 
   ${
@@ -506182,12 +506228,12 @@ strict in the case where the sets B(x) overlap.  (Contributed by Thierry
        (Contributed by Thierry Arnoux, 21-Jan-2017.) $)
     orvcval4 $p |- ( ph ->
                         ( X oRVC R A ) = ( `' X " { y e. U. J | y R A } ) ) $=
-      ( cima cuni co wceq ctop wf wcel cvv ccnv wbr cab cin corvc crab wfun crn
-      cv wss csigagen sgsiga isanmbfm mbfmfun mbfmf elex unisg 3syl feq3d mpbid
+      ( cima cuni co wceq wf ctop wcel cvv ccnv wbr cab cin corvc crab wfun crn
+      cv wss csigagen isanmbfm mbfmfun sgsiga mbfmf elex unisg 3syl feq3d mpbid
       cfv frnd fimacnvinrn2 syl2anc cmbfm orvcval dfrab2 a1i imaeq2d 3eqtr4d )
       AHUAZBUICDUBZBUCZMZVKVMFNZUDZMZHCDUEOVKVLBVOUFZMAHUGHUHVOUJVNVQPAHAEFUKVA
-      ZHIAFQJULZKUMUNZAENZVOHAWBVSNZHRWBVOHRAEVSHIVTKUOAWCVOHWBAFQSFTSWCVOPJFQU
-      PFTUQURUSUTVBVMVOHVCVDABCDEVSVEOGHWAKLVFAVRVPVKVRVPPAVLBVOVGVHVIVJ $.
+      ZHKULUMZAENZVOHAWAVSNZHQWAVOHQAEVSHIAFRJUNKUOAWBVOHWAAFRSFTSWBVOPJFRUPFTU
+      QURUSUTVBVMVOHVCVDABCDEVSVEOGHVTKLVFAVRVPVKVRVPPAVLBVOVGVHVIVJ $.
 
     ${
       orvcoel.5 $e |- ( ph -> { y e. U. J | y R A } e. J ) $.
@@ -656642,6 +656688,27 @@ D Fn ( I ... ( M - 1 ) ) /\
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
+  ${
+    ressbasssg.r $e |- R = ( W |`s A ) $.
+    ressbasssg.b $e |- B = ( Base ` W ) $.
+    $( The base set of a restriction to ` A ` is a subset of ` A ` and the base
+       set ` B ` of the original structure.  (Contributed by SN,
+       10-Jan-2025.) $)
+    ressbasssg $p |- ( Base ` R ) C_ ( A i^i B ) $=
+      ( cvv wcel cbs cfv cin wss ressbas ssid eqsstrrdi wn c0 cress reldmress
+      co ovprc2 eqtrid fveq2d base0 0ss eqsstrri eqsstrdi pm2.61i ) AGHZCIJZABK
+      ZLUIUJUKUKABCGDEFMUKNOUIPZUJQIJZUKULCQIULCDARTQEDARSUAUBUCUMQUKUDUKUEUFUG
+      UH $.
+  $}
+
+  ${
+    ressbasss2.r $e |- R = ( W |`s A ) $.
+    $( The base set of a restriction to ` A ` is a subset of ` A ` .
+       (Contributed by SN, 10-Jan-2025.) $)
+    ressbasss2 $p |- ( Base ` R ) C_ A $=
+      ( cbs cfv cin eqid ressbasssg inss1 sstri ) BEFACEFZGAALBCDLHIALJK $.
+  $}
+
   ${
     nelsubginvcld.g $e |- ( ph -> G e. Grp ) $.
     nelsubginvcld.s $e |- ( ph -> S e. ( SubGrp ` G ) ) $.
@@ -657078,6 +657145,73 @@ D Fn ( I ... ( M - 1 ) ) /\
       ( ringabld ablcmnd ) ABABCDE $.
   $}
 
+  ${
+    $d C a b x y $.  $d F a b $.  $d M a b $.  $d ph a b x y $.
+    rncrhmcl.c $e |- C = ( N |`s ran F ) $.
+    rncrhmcl.h $e |- ( ph -> F e. ( M RingHom N ) ) $.
+    rncrhmcl.m $e |- ( ph -> M e. CRing ) $.
+    $( The range of a commutative ring homomorphism is a commutative ring.
+       (Contributed by SN, 10-Jan-2025.) $)
+    rncrhmcl $p |- ( ph -> C e. CRing ) $=
+      ( vx vy va vb wcel cv cmulr cfv co wceq wa eqid crg cbs wral ccrg crh crn
+      csubrg rnrhmsubrg subrgring 3syl ressbasss2 sseli anim12i wfn wrex wf syl
+      rhmf ffnd simpl fvelrnb biimpa syl2an simpr adantr simplrl simprl crngcom
+      ad3antrrr syl3anc fveq2d rhmmul 3eqtr3d cvv rnexg ressmulr simplrr simprr
+      oveq123d rexlimddv sylan2 ralrimivva iscrng2 sylanbrc ) ABUAMZINZJNZBOPZQ
+      ZWGWFWHQZRZJBUBPZUCIWLUCBUDMACDEUEQZMZCUFZEUGPMWEGCDEUHWOEBFUIUJAWKIJWLWL
+      WFWLMZWGWLMZSAWFWOMZWGWOMZSZWKWPWRWQWSWLWOWFWOBEFUKZULWLWOWGXAULUMAWTSZKN
+      ZCPZWFRZWKKDUBPZACXFUNZWRXEKXFUOZWTAXFEUBPZCAWNXFXICUPGXFXIDECXFTZXITURUQ
+      USZWRWSUTXGWRXHKXFWFCVAVBVCXBXCXFMZXESZSZLNZCPZWGRZWKLXFXBXQLXFUOZXMAXGWS
+      XRWTXKWRWSVDXGWSXRLXFWGCVAVBVCVEXNXOXFMZXQSZSZXDXPEOPZQZXPXDYBQZWIWJYAXCX
+      ODOPZQZCPZXOXCYEQZCPZYCYDYAYFYHCYADUDMZXLXSYFYHRAYJWTXMXTHVIXBXLXEXTVFZXN
+      XSXQVGZXFDYEXCXOXJYETZVHVJVKYAWNXLXSYGYCRAWNWTXMXTGVIZYKYLXCXODEYEYBCXFXJ
+      YMYBTZVLVJYAWNXSXLYIYDRYNYLYKXOXCDEYEYBCXFXJYMYOVLVJVMYAXDWFXPWGYBWHAYBWH
+      RZWTXMXTAWNWOVNMYPGCWMVOWOEBYBVNFYOVPUJVIZXBXLXEXTVQZXNXSXQVRZVSYAXPWGXDW
+      FYBWHYQYSYRVSVMVTVTWAWBIJWLBWHWLTWHTWCWD $.
+  $}
+
+  $( The converse of a ring isomorphism is a ring isomorphism.  (Contributed by
+     SN, 10-Jan-2025.) $)
+  rimcnv $p |- ( F e. ( R RingIso S ) -> `' F e. ( S RingIso R ) ) $=
+    ( crh co wcel ccnv wa crs cbs cfv wf wceq eqid rhmf wrel frel dfrel2 isrim0
+    sylib syl id eqeltrd anim1ci 3imtr4i ) CABDEZFZCGZBADEFZHUIUHGZUFFZHCABIEFU
+    HBAIEFUGUKUIUGUJCUFUGAJKZBJKZCLZUJCMZULUMABCULNUMNOUNCPUOULUMCQCRTUAUGUBUCU
+    DABCSBAUHSUE $.
+
+  $( Prove isomorphic by an explicit isomorphism.  (Contributed by SN,
+     10-Jan-2025.) $)
+  brrici $p |- ( F e. ( R RingIso S ) -> R ~=r S ) $=
+    ( crs co wcel c0 wne cric wbr ne0i brric sylibr ) CABDEZFNGHABIJNCKABLM $.
+
+  ${
+    $d R f $.  $d S f $.
+    $( Ring isomorphism is symmetric.  (Contributed by SN, 10-Jan-2024.) $)
+    ricsym $p |- ( R ~=r S -> S ~=r R ) $=
+      ( vf cric wbr crs co c0 wne brric wcel wex ccnv rimcnv brrici syl exlimiv
+      cv n0 sylbi ) ABDEABFGZHIZBADEZABJUBCRZUAKZCLUCCUASUEUCCUEUDMZBAFGKUCABUD
+      NBAUFOPQTT $.
+  $}
+
+  ${
+    $d R f $.  $d S f $.
+    $( Ring isomorphism preserves (multiplicative) commutativity.  (Contributed
+       by SN, 10-Jan-2025.) $)
+    riccrng1 $p |- ( ( R ~=r S /\ R e. CRing ) -> S e. CRing ) $=
+      ( vf cric wbr cv crs co wcel wex ccrg c0 wne wceq cbs cfv eqid cvv adantr
+      cress brric n0 bitri wi crn wf1o wfo rimf1o f1ofo forn 3syl oveq2d rimrcl
+      wa ressid simpl2im eqtr2d rimrhm simpr rncrhmcl eqeltrd ex exlimiv sylanb
+      crh imp ) ABDEZCFZABGHZIZCJZAKIZBKIZVGVILMVKABUACVIUBUCVKVLVMVJVLVMUDCVJV
+      LVMVJVLUNZBBVHUEZTHZKVJBVPNVLVJVPBBOPZTHZBVJVOVQBTVJAOPZVQVHUFVSVQVHUGVOV
+      QNVSVQABVHVSQVQQZUHVSVQVHUIVSVQVHUJUKULVJARIBRIVRBNABVHUMVQBRVTUOUPUQSVNV
+      PVHABVPQVJVHABVEHIVLABVHURSVJVLUSUTVAVBVCVFVD $.
+  $}
+
+  $( A ring is commutative if and only if an isomorphic ring is commutative.
+     (Contributed by SN, 10-Jan-2025.) $)
+  riccrng $p |- ( R ~=r S -> ( R e. CRing <-> S e. CRing ) ) $=
+    ( cric wbr ccrg wcel riccrng1 ricsym sylan impbida ) ABCDZAEFZBEFZABGKBACDM
+    LABHBAGIJ $.
+
   ${
     drnginvrcld.b $e |- B = ( Base ` R ) $.
     drnginvrcld.0 $e |- .0. = ( 0g ` R ) $.
@@ -660934,33 +661068,30 @@ evaluates to zero (the "zero set").  (In other words, scalar multiples
     $( The "curve" (zero set) corresponding to the zero polynomial contains all
        coordinates.  (Contributed by SN, 23-Nov-2024.) $)
     prjcrv0 $p |- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) $=
-      ( va co cfv cc0 cv wceq eqid wcel cvv vp vn vf vg vh vk cprjcrv cevl cima
-      cfz c0g csn crab cmhp wfun crn cuni cn0 csupp ccnfld cress cgsu ccnv cmap
-      cn cfn wss cbs cmpt funmpt cfield mhpfval funeqd mpbiri fldcrngd crnggrpd
-      ovexd cxp mpl0 0nn0 a1i mhp0cl eqeltrd elunirn2 syl2anc prjcrvval wa ccrg
-      adantr evl0 imaeq1d cin c0 wne cfrlm cdif ciun wrex cprjspn eleq2i biimpi
-      clspn adantl cprjsp cdr isfld simplbi syl prjspnval clvec prjspval2 eqtrd
-      frlmlvec eleqtrd eliun sylib cfsupp wbr frlmbas ssrab2 eqsstrrdi ad2antrr
-      eldifi adantrr sseldd wel velsn anbi2i lveclmodd lspsnid wn eldifn eldifd
+      ( vp va co cfv cc0 wceq eqid wcel cvv vh vk cprjcrv cfz cevl cima c0g csn
+      cv crab cmhp crn cuni ccnv cfn cn0 cmap ovexd fldcrngd crnggrpd mpl0 0nn0
+      cn cxp a1i mhp0cl eqeltrd elfvunirn syl prjcrvval wa cbs ccrg adantr evl0
+      imaeq1d cin c0 wne cfrlm clspn cdif ciun wrex eleq2i biimpi adantl cprjsp
+      cprjspn cdr cfield isfld simplbi prjspnval clvec frlmlvec prjspval2 eqtrd
+      syl2anc eleqtrd eliun sylib wss cfsupp wbr frlmbas ssrab2 ad2antrr eldifi
+      eqsstrrdi adantrr sseldd wel velsn anbi2i lveclmodd lspsnid eldifn eldifd
       clmod eleq2 syl5ibrcom impr sylan2b elind ne0d rexlimddv xpima2 rabeqcda
-      ) AFDCUGMNFODUJMZCUHMZNZUAPZUIZCUKNZULZQZUABUMBABUUEFUUDCUNMZCDUUIUAUULRZ
-      UUERZIUUIRZJKAUULUOZFOUULNZSFUULUPUQSAUUPUBURUCPUUIUSMUTURVAMUDPVBMUBPQUD
-      UEPVCVEUIVFSUEURUUDVDMUMZUMVGUCEVHNZUMZVIZUOUBURUUTVJAUULUVAAUUSUURECUCUD
-      UEUBUULUUDTVKUUIUUMGUUSRUUOUURRZAODUJVQZKVLVMVNAFUURUUJVRUUQAUURECUEUUDUU
-      ITFGUVBUUOHUVCACACKVOZVPZVSAUURCUEUULUUDOTUUIUUMUUOUVBUVCUVEOURSAVTWAWBWC
-      OFUULWDWEWFAUUKUABAUUGBSZWGZUUHCVHNZUUDVDMZUUJVRZUUGUIZUUJUVGUUFUVJUUGUVG
-      UVHUUECUUDUUITEFUUNUVHRZGUUOHUVGODUJVQACWHSZUVFUVDWIWJWKUVGUVIUUGWLZWMWNZ
-      UVKUUJQUVGUUGLPZULCUUDWOMZXBNZNZUVQUKNZULZWPZULZSZUVOLUVQVHNZUWAWPZUVGUUG
-      LUWFUWCWQZSUWDLUWFWRUVGUUGDCWSMZUWGUVFUUGUWHSZAUVFUWIBUWHUUGIWTXAXCUVGUWH
-      UVQXDNZUWGUVGDURSZCXESZUWHUWJQAUWKUVFJWIAUWLUVFACVKSZUWLKUWMUWLUVMCXFXGXH
-      ZWICDXIWEUVGUVQXJSZUWJUWGQAUWOUVFAUWLUUDTSZUWOUWNUVCCUVQUUDTUVQRZXMWEZWIL
-      UWFUVRUVQUVTUVTRUWFRUVRRZXKXHXLXNLUUGUWFUWCXOXPUVGUVPUWFSZUWDWGZWGZUVNUVP
-      UXBUVIUUGUVPUXBUWEUVIUVPAUWEUVIVGUVFUXAAUWEUFPUUIXQXRZUFUVIUMZUVIAUWMUWPU
-      XDUWEQKUVCUXDCUFUVQUUDUVHVKTUUIUWQUVLUUOUXDRXSWEUXCUFUVIXTYAYBUVGUWTUVPUW
-      ESZUWDUWTUXEUVGUVPUWEUWAYCXCZYDYEUXAUVGUWTUUGUWBQZWGLUAYFZUWDUXGUWTUAUWBY
-      GYHUVGUWTUXGUXHUVGUWTWGZUXHUXGUVPUWBSUXIUVPUVSUWAUXIUVQYNSZUXEUVPUVSSAUXJ
-      UVFUWTAUVQUWRYIYBUXFUVRUWEUVQUVPUWERUWSYJWEUWTUVPUWASYKUVGUVPUWEUWAYLXCYM
-      UUGUWBUVPYOYPYQYRYSYTUUAUVIUUJUUGUUBXHXLUUCXL $.
+      wn ) AFDCUCNOFPDUDNZCUENZOZLUIZUFZCUGOZUHZQZLBUJBABYLFYKCUKNZCDYPLYSRZYLR
+      ZIYPRZJKAFPYSOZSFYSULUMSAFUAUIUNVCUFUOSUAUPYKUQNUJZYQVDUUCAUUDECUAYKYPTFG
+      UUDRZUUBHAPDUDURZACACKUSZUTZVAAUUDCUAYSYKPTYPYTUUBUUEUUFUUHPUPSAVBVEVFVGP
+      FYSVHVIVJAYRLBAYNBSZVKZYOCVLOZYKUQNZYQVDZYNUFZYQUUJYMUUMYNUUJUUKYLCYKYPTE
+      FUUAUUKRZGUUBHUUJPDUDURACVMSZUUIUUGVNVOVPUUJUULYNVQZVRVSZUUNYQQUUJYNMUIZU
+      HCYKVTNZWAOZOZUUTUGOZUHZWBZUHZSZUURMUUTVLOZUVDWBZUUJYNMUVIUVFWCZSUVGMUVIW
+      DUUJYNDCWINZUVJUUIYNUVKSZAUUIUVLBUVKYNIWEWFWGUUJUVKUUTWHOZUVJUUJDUPSZCWJS
+      ZUVKUVMQAUVNUUIJVNAUVOUUIACWKSZUVOKUVPUVOUUPCWLWMVIZVNCDWNWSUUJUUTWOSZUVM
+      UVJQAUVRUUIAUVOYKTSZUVRUVQUUFCUUTYKTUUTRZWPWSZVNMUVIUVAUUTUVCUVCRUVIRUVAR
+      ZWQVIWRWTMYNUVIUVFXAXBUUJUUSUVISZUVGVKZVKZUUQUUSUWEUULYNUUSUWEUVHUULUUSAU
+      VHUULXCUUIUWDAUVHUBUIYPXDXEZUBUULUJZUULAUVPUVSUWGUVHQKUUFUWGCUBUUTYKUUKWK
+      TYPUVTUUOUUBUWGRXFWSUWFUBUULXGXJXHUUJUWCUUSUVHSZUVGUWCUWHUUJUUSUVHUVDXIWG
+      ZXKXLUWDUUJUWCYNUVEQZVKMLXMZUVGUWJUWCLUVEXNXOUUJUWCUWJUWKUUJUWCVKZUWKUWJU
+      USUVESUWLUUSUVBUVDUWLUUTXTSZUWHUUSUVBSAUWMUUIUWCAUUTUWAXPXHUWIUVAUVHUUTUU
+      SUVHRUWBXQWSUWCUUSUVDSYJUUJUUSUVHUVDXRWGXSYNUVEUUSYAYBYCYDYEYFYGUULYQYNYH
+      VIWRYIWR $.
   $}
 
 
@@ -700489,11 +700620,6 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
       ABOPQRZOSPTZCDUAZUBZOCDEFGBOUIUKBUIUCUJBCDUJBUDHIUEUFHIJULUGKLMNUH $.
   $}
 
-  $( A member of a union that is not a member of the second class, is a member
-     of the first class.  (Contributed by Glauco Siliprandi, 11-Dec-2019.) $)
-  elunnel2 $p |- ( ( A e. ( B u. C ) /\ -. A e. C ) -> A e. B ) $=
-    ( cun wcel wo elun biimpi orcomd orcanai ) ABCDEZACEZABEZKMLKMLFABCGHIJ $.
-
   ${
     adantlllr.1 $e |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta ) $.
     $( Deduction adding a conjunct to antecedent.  (Contributed by Glauco
@@ -776541,24 +776667,22 @@ subcategory subset of the mappings between base sets of unital rings (in
         ( co wa wcel wceq wbr csect cfv crh ccom cid cbs cres crs ccnv ringccat
         ccat syl isinv w3a ringcsect df-3an bitrdi 3ancoma bitri anbi12d anandi
         eqid wf1o simplrl adantl wf rhmf anim12i ad2antlr simpr ad2antrl fcof1o
-        jca32 eqcom anbi2i sylib anass sylanbrc wb syl2anc anbi1d adantr mpbird
-        isrim rimrhm isrim0 eleq1 eqcoms anbi2d sylan9bbr syl6bi expdimp impcom
-        com12 coeq1 ad2antll rimf1o f1ococnv1 eqtrd jca31 biimpcd coeq2 impbida
-        wi f1ococnv2 3bitrd ) AEFIJGQUAEFIJCUBUCZQUAZFEJIXHQUAZRZEIJUDQSZFJIUDQ
-        ZSZRZFEUEZUFIUGUCZUHZTZRZXORZXTEFUEZUFJUGUCZUHZTZRZRZEIJUIQSZFEUJZTZRZA
-        BCXHEFGIJLPADHSCULSMCDHKUKUMNOXHVCZUNAXKXTXOYERZRYGAXIXTXJYMAXIXLXNXSUO
-        XTABCXHDXQEFHIJKLMNOXQVCZYLUPXLXNXSUQURAXJXNXLYEUOZYMABCXHDYCFEHJIKLMON
-        YCVCZYLUPYOXLXNYEUOYMXNXLYEUSXLXNYEUQUTURVAXTXOYEVBURAYGYKAYGRZYKXLXQYC
-        EVDZRZYJRZYQXLYRYJRZYTYGXLAXTXLXNYFVEVFYQXQYCEVGZYCXQFVGZRZYEXSRRZUUAYG
-        UUEAYGUUDYEXSXOUUDXTYFXLUUBXNUUCXQYCIJEYNYPVHYCXQJIFYPYNVHVIVJYFYEYAXTY
-        EVKVFXTXSYAYEXOXSVKVLVNVFUUEYRYIFTZRUUAXQYCEFVMUUFYJYRYIFVOVPVQUMXLYRYJ
-        VRVSAYKYTVTYGAYHYSYJAIBSZJBSZYHYSVTNOXQYCIJEBBYNYPWEWAWBWCWDAYKRZXTXOYF
-        UUIXLXNXSYHXLAYJXQYCIJEYNYPWFVLYKAXNYHYJAXNYJARZYHXNUUJYHXOXNAYHXLYIXMS
-        ZRZYJXOAUUGUUHYHUULVTNOIJEBBWGWAZYJUUKXNXLUUKXNVTYIFYIFXMWHWIWJWKXLXNVK
-        WLWOWMWNUUIXPYIEUEZXRYJXPUUNTAYHFYIEWPWQUUIYRUUNXRTYHYRAYJXQYCIJEYNYPWR
-        VLZXQYCEWSUMWTZXAUUIXOUULYKAUULYHAUULXEYJAYHUULUUMXBWCWNUUIXNUUKXLYJXNU
-        UKVTAYHFYIXMWHWQWJWDZUUIXOXSYEUUQUUPUUIYBEYIUEZYDYJYBUURTAYHFYIEXCWQUUI
-        YRUURYDTUUOXQYCEXFUMWTXAXAXDXG $.
+        jca32 eqcom anbi2i sylib anass sylanbrc a1i anbi1d adantr mpbird rimrhm
+        wb isrim isrim0 simprbi eleq1 syl5ibrcom coeq1 ad2antll f1ococnv1 eqtrd
+        imp rimf1o jca31 biimpi anbi2d coeq2 f1ococnv2 impbida 3bitrd ) AEFIJGQ
+        UAEFIJCUBUCZQUAZFEJIXDQUAZRZEIJUDQSZFJIUDQZSZRZFEUEZUFIUGUCZUHZTZRZXKRZ
+        XPEFUEZUFJUGUCZUHZTZRZRZEIJUIQSZFEUJZTZRZABCXDEFGIJLPADHSCULSMCDHKUKUMN
+        OXDVCZUNAXGXPXKYARZRYCAXEXPXFYIAXEXHXJXOUOXPABCXDDXMEFHIJKLMNOXMVCZYHUP
+        XHXJXOUQURAXFXJXHYAUOZYIABCXDDXSFEHJIKLMONXSVCZYHUPYKXHXJYAUOYIXJXHYAUS
+        XHXJYAUQUTURVAXPXKYAVBURAYCYGAYCRZYGXHXMXSEVDZRZYFRZYMXHYNYFRZYPYCXHAXP
+        XHXJYBVEVFYMXMXSEVGZXSXMFVGZRZYAXORRZYQYCUUAAYCYTYAXOXKYTXPYBXHYRXJYSXM
+        XSIJEYJYLVHXSXMJIFYLYJVHVIVJYBYAXQXPYAVKVFXPXOXQYAXKXOVKVLVNVFUUAYNYEFT
+        ZRYQXMXSEFVMUUBYFYNYEFVOVPVQUMXHYNYFVRVSAYGYPWEYCAYDYOYFYDYOWEAXMXSIJEY
+        JYLWFVTWAWBWCAYGRZXPXKYBUUCXHXJXOYDXHAYFIJEWDVLYGXJAYDYFXJYDXJYFYEXISZY
+        DXHUUDIJEWGZWHFYEXIWIZWJWOVFUUCXLYEEUEZXNYFXLUUGTAYDFYEEWKWLUUCYNUUGXNT
+        YDYNAYFXMXSIJEYJYLWPVLZXMXSEWMUMWNZWQUUCXKXHUUDRZYDUUJAYFYDUUJUUEWRVLUU
+        CXJUUDXHYFXJUUDWEAYDUUFWLWSWCZUUCXKXOYAUUKUUIUUCXREYEUEZXTYFXRUULTAYDFY
+        EEWTWLUUCYNUULXTTUUHXMXSEXAUMWNWQWQXBXC $.
     $}
 
     ${
@@ -776961,25 +777085,23 @@ the category of sets which sends each ring to its underlying set (base
         ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) ) $=
         ( co wa wcel wceq wbr csect cfv crh ccom cid cbs cres ccnv ringccatALTV
         crs ccat syl eqid isinv w3a ringcsectALTV df-3an bitrdi 3ancoma anbi12d
-        bitri anandi wf1o simplrl adantl wf anim12i ad2antlr simpr ad2antrl jca
-        fcof1o eqcom anbi2i sylib anass sylanbrc wb anbi1d adantr mpbird rimrhm
-        rhmf isrim isrim0 eleq1 eqcoms anbi2d syl6bi com12 expdimp impcom coeq1
-        sylan9bbr ad2antll rimf1o f1ococnv1 eqtrd jca31 biimpcd coeq2 f1ococnv2
-        wi impbida 3bitrd ) AEFIJGQUAEFIJCUBUCZQUAZFEJIXGQUAZRZEIJUDQSZFJIUDQZS
-        ZRZFEUEZUFIUGUCZUHZTZRZXNRZXSEFUEZUFJUGUCZUHZTZRZRZEIJUKQSZFEUIZTZRZABC
-        XGEFGIJLPADHSCULSMCDHKUJUMNOXGUNZUOAXJXSXNYDRZRYFAXHXSXIYLAXHXKXMXRUPXS
-        ABCXGDXPEFHIJKLMNOXPUNZYKUQXKXMXRURUSAXIXMXKYDUPZYLABCXGDYBFEHJIKLMONYB
-        UNZYKUQYNXKXMYDUPYLXMXKYDUTXKXMYDURVBUSVAXSXNYDVCUSAYFYJAYFRZYJXKXPYBEV
-        DZRZYIRZYPXKYQYIRZYSYFXKAXSXKXMYEVEVFYPXPYBEVGZYBXPFVGZRZYDXRRZRZYTYFUU
-        EAYFUUCUUDXNUUCXSYEXKUUAXMUUBXPYBIJEYMYOWDYBXPJIFYOYMWDVHVIYFYDXRYEYDXT
-        XSYDVJVFXSXRXTYDXNXRVJVKVLVLVFUUEYQYHFTZRYTXPYBEFVMUUFYIYQYHFVNVOVPUMXK
-        YQYIVQVRAYJYSVSYFAYGYRYIAIBSZJBSZRZYGYRVSAUUGUUHNOVLZXPYBIJEBBYMYOWEUMV
-        TWAWBAYJRZXSXNYEUUKXKXMXRYGXKAYIXPYBIJEYMYOWCVKYJAXMYGYIAXMYIARZYGXMUUL
-        YGXNXMAYGXKYHXLSZRZYIXNAUUIYGUUNVSUUJIJEBBWFUMZYIUUMXMXKUUMXMVSYHFYHFXL
-        WGWHWIWOXKXMVJWJWKWLWMUUKXOYHEUEZXQYIXOUUPTAYGFYHEWNWPUUKYQUUPXQTYGYQAY
-        IXPYBIJEYMYOWQVKZXPYBEWRUMWSZWTUUKXNUUNYJAUUNYGAUUNXDYIAYGUUNUUOXAWAWMU
-        UKXMUUMXKYIXMUUMVSAYGFYHXLWGWPWIWBZUUKXNXRYDUUSUURUUKYAEYHUEZYCYIYAUUTT
-        AYGFYHEXBWPUUKYQUUTYCTUUQXPYBEXCUMWSWTWTXEXF $.
+        bitri anandi wf1o simplrl wf rhmf anim12i ad2antlr simpr ad2antrl jca32
+        adantl fcof1o eqcom anbi2i sylib anass sylanbrc isrim a1i anbi1d adantr
+        mpbird rimrhm isrim0 simprbi eleq1 syl5ibrcom imp coeq1 ad2antll rimf1o
+        wb f1ococnv1 eqtrd jca31 biimpi anbi2d coeq2 f1ococnv2 impbida 3bitrd )
+        AEFIJGQUAEFIJCUBUCZQUAZFEJIXDQUAZRZEIJUDQSZFJIUDQZSZRZFEUEZUFIUGUCZUHZT
+        ZRZXKRZXPEFUEZUFJUGUCZUHZTZRZRZEIJUKQSZFEUIZTZRZABCXDEFGIJLPADHSCULSMCD
+        HKUJUMNOXDUNZUOAXGXPXKYARZRYCAXEXPXFYIAXEXHXJXOUPXPABCXDDXMEFHIJKLMNOXM
+        UNZYHUQXHXJXOURUSAXFXJXHYAUPZYIABCXDDXSFEHJIKLMONXSUNZYHUQYKXHXJYAUPYIX
+        JXHYAUTXHXJYAURVBUSVAXPXKYAVCUSAYCYGAYCRZYGXHXMXSEVDZRZYFRZYMXHYNYFRZYP
+        YCXHAXPXHXJYBVEVMYMXMXSEVFZXSXMFVFZRZYAXORRZYQYCUUAAYCYTYAXOXKYTXPYBXHY
+        RXJYSXMXSIJEYJYLVGXSXMJIFYLYJVGVHVIYBYAXQXPYAVJVMXPXOXQYAXKXOVJVKVLVMUU
+        AYNYEFTZRYQXMXSEFVNUUBYFYNYEFVOVPVQUMXHYNYFVRVSAYGYPWNYCAYDYOYFYDYOWNAX
+        MXSIJEYJYLVTWAWBWCWDAYGRZXPXKYBUUCXHXJXOYDXHAYFIJEWEVKYGXJAYDYFXJYDXJYF
+        YEXISZYDXHUUDIJEWFZWGFYEXIWHZWIWJVMUUCXLYEEUEZXNYFXLUUGTAYDFYEEWKWLUUCY
+        NUUGXNTYDYNAYFXMXSIJEYJYLWMVKZXMXSEWOUMWPZWQUUCXKXHUUDRZYDUUJAYFYDUUJUU
+        EWRVKUUCXJUUDXHYFXJUUDWNAYDUUFWLWSWDZUUCXKXOYAUUKUUIUUCXREYEUEZXTYFXRUU
+        LTAYDFYEEWTWLUUCYNUULXTTUUHXMXSEXAUMWPWQWQXBXC $.
     $}
 
     ${