Revise proof of fsumf1o in iset.mm

Uses fsum3 instead of fisum .

Author: jkingdon

iset-discouraged

@@ -150,7 +150,6 @@
 "eu3h" is used by "2eu4".
 "eu3h" is used by "eu3".
 "eu3h" is used by "mo2r".
-"fisum" is used by "fsumf1o".
 "fisumcvg" is used by "fisumcvg2".
 "fisumcvg" is used by "isummolem2a".
 "fisumcvg2" is used by "fisumsers".
@@ -389,7 +388,7 @@ New usage of "elirr" is discouraged (16 uses).
 New usage of "equsalh" is discouraged (5 uses).
 New usage of "eu3h" is discouraged (3 uses).
 New usage of "exmidfodomrlemrALT" is discouraged (0 uses).
-New usage of "fisum" is discouraged (1 uses).
+New usage of "fisum" is discouraged (0 uses).
 New usage of "fisumcvg" is discouraged (2 uses).
 New usage of "fisumcvg2" is discouraged (1 uses).
 New usage of "fisumser" is discouraged (2 uses).

iset.mm

@@ -115860,27 +115860,26 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
     fsumf1o $p |- ( ph -> sum_ k e. A B = sum_ n e. C D ) $=
       ( vm c0 wceq cfv wcel cc vf csu chash cn c1 cfz co cv wf1o wex wa cc0 wfo
       sum0 f1oeq2 syl5ibcom imp f1ofo fo00 simprbi sumeq1d simpr syl6eq 3eqtr4a
-      3syl ex cmpt caddc cle wbr ccom cseq4 2fveq3 simprl simprr f1of ffvelrnda
-      cif wf syl fmpttd syldan adantlr adantr f1oco fvco3 sylan ad2antll fveq2d
-      syl2anc eqtrd wral eqeltrrd eleq1d ralrimiva rspcdva eqid fvmptg 3eqtr4rd
-      fisum fvmpt2 nffvmpt1 nfeq1 fveq2 eqeq12d rspc mpan9 sumeq2dv sumfct expr
+      3syl ex cmpt caddc cle wbr ccom cif cseq 2fveq3 simprl simprr wf f1of syl
+      ffvelrnda fmpttd syldan adantlr adantr f1oco syl2anc fvco3 sylan ad2antll
+      fveq2d eqtrd wral eqid eqeltrrd eleq1d ralrimiva rspcdva fvmptd3 3eqtr4rd
+      fsum3 fvmpt2 nffvmpt1 nfeq1 fveq2 eqeq12d rspc mpan9 sumeq2dv sumfct expr
       3eqtr3d exlimdv expimpd cfn wo fz1f1o mpjaod ) ADPQZBCFUBZDEGUBZQZDUCRZUD
       SZUEYBUFUGZDUAUHZUIZUAUJZUKZAXRYAAXRUKZPCFUBULXSXTCFUNYIBPCFYIPBHUIZPBHUM
       ZBPQZAXRYJADBHUIZXRYJLDPBHUOUPUQPBHURYKHPQYLBHUSUTVEVAYIXTPEGUBULYIDPEGAX
       RVBVAEGUNVCVDVFAYCYGYAAYCUKYFYAUAAYCYFYAAYCYFUKZUKZBOUHZFBCVGZRZOUBZDYPGD
-      EVGZRZOUBZXSXTYODYPHRZYQRZOUBYBVHTGUDGUHZYBVIVJUUEYQHYEVKZVKZRZULVRVGUEVL
-      RUUBYSYODUUDUUEYERZHRZYQRZOGYEUUGYBYPUUIYQHVMAYCYFVNZAYCYFVOZAYPDSZUUDTSZ
-      YNAUUNUUCBSUUOADBYPHAYMDBHVSLDBHVPVTZVQABTUUCYQAFBCTNWAZVQWBWCYOUUEYDSZUK
-      ZUUHUUEUUFRZYQRZUUKYOYDBUUFVSZUURUUHUVAQYOYDBUUFUIZUVBYOYMYFUVCAYMYNLWDUU
-      MYDDBHYEWEWJZYDBUUFVPVTYDBUUEYQUUFWFWGZUUSUUTUUJYQYOYDDYEVSZUURUUTUUJQYFU
-      VFAYCYDDYEVPWHYDDUUEHYEWFWGWIWKWTYODUUAUUDOAUUNUUAUUDQZYNAUUEYTRZUUEHRZYQ
-      RZQZGDWLUUNUVGAUVKGDAUUEDSZUKZIYQRZEUVJUVHUVMIBSETSZUVNEQUVMUVIIBMADBUUEH
-      UUPVQWMZUVMCTSZUVOFBIFUHIQCETJWNAUVQFBWLZUVLAUVQFBNWOZWDUVPWPZFICEBTYQJYQ
-      WQWRWJUVMUVIIYQMWIUVMUVLUVOUVHEQAUVLVBUVTGDETYTYTWQXAWJWSWOUVKUVGGYPDGUUA
-      UUDGDEYPXBXCUUEYPQUVHUUAUVJUUDUUEYPYTXDUUEYPYQHVMXEXFXGWCXHYOBYRUVAOGUUFU
-      UGYBYPUUTYQXDUULUVDYOBTYPYQABTYQVSYNUUQWDVQUVEWTWSAYSXSQZYNAUVRUWAUVSBCOF
-      XIVTWDAUUBXTQZYNAUVOGDWLUWBAUVOGDUVTWODEOGXIVTWDXKXJXLXMADXNSXRYHXOKDUAXP
-      VTXQ $.
+      EVGZRZOUBZXSXTYODYPHRZYQRZOUBYBVHGUDGUHZYBVIVJUUEYQHYEVKZVKZRZULVLVGUEVMR
+      UUBYSYODUUDUUEYERZHRZYQRZOGYEUUGYBYPUUIYQHVNAYCYFVOZAYCYFVPZAYPDSZUUDTSZY
+      NAUUNUUCBSUUOADBYPHAYMDBHVQLDBHVRVSZVTABTUUCYQAFBCTNWAZVTWBWCYOUUEYDSZUKZ
+      UUHUUEUUFRZYQRZUUKYOYDBUUFVQZUURUUHUVAQYOYDBUUFUIZUVBYOYMYFUVCAYMYNLWDUUM
+      YDDBHYEWEWFZYDBUUFVRVSYDBUUEYQUUFWGWHZUUSUUTUUJYQYOYDDYEVQZUURUUTUUJQYFUV
+      FAYCYDDYEVRWIYDDUUEHYEWGWHWJWKWTYODUUAUUDOAUUNUUAUUDQZYNAUUEYTRZUUEHRZYQR
+      ZQZGDWLUUNUVGAUVKGDAUUEDSZUKZIYQREUVJUVHUVMFICEBYQTYQWMJUVMUVIIBMADBUUEHU
+      UPVTWNZUVMCTSZETSZFBIFUHIQCETJWOAUVOFBWLZUVLAUVOFBNWPZWDUVNWQZWRUVMUVIIYQ
+      MWJUVMUVLUVPUVHEQAUVLVBUVSGDETYTYTWMXAWFWSWPUVKUVGGYPDGUUAUUDGDEYPXBXCUUE
+      YPQUVHUUAUVJUUDUUEYPYTXDUUEYPYQHVNXEXFXGWCXHYOBYRUVAOGUUFUUGYBYPUUTYQXDUU
+      LUVDYOBTYPYQABTYQVQYNUUQWDVTUVEWTWSAYSXSQZYNAUVQUVTUVRBCOFXIVSWDAUUBXTQZY
+      NAUVPGDWLUWAAUVPGDUVSWPDEOGXIVSWDXKXJXLXMADXNSXRYHXOKDUAXPVSXQ $.
   $}
 
   ${