:: REARRAN1 semantic presentation begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set (Const "E")); let "r" be ($#m1_subset_1 :::"Real":::); :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "F" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); end; definitionlet "IT" be ($#m1_hidden :::"FinSequence":::); attr "IT" is :::"terms've_same_card_as_number"::: means :: REARRAN1:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "IT"))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))); attr "IT" is :::"ascending"::: means :: REARRAN1:def 2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "IT" ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"terms've_same_card_as_number"::: REARRAN1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))))) "holds" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ")" )); :: deftheorem defines :::"ascending"::: REARRAN1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_rearran1 :::"ascending"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "X")); attr "IT" is :::"lenght_equal_card_of_set"::: means :: REARRAN1:def 3 (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "X")) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) "IT") ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )); end; :: deftheorem defines :::"lenght_equal_card_of_set"::: REARRAN1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set (Var "X")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) "D") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v2_rearran1 :::"ascending"::: ) ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "D"); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; mode RearrangmentGen of "D" is ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v2_rearran1 :::"ascending"::: ) ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "D"); end; theorem :: REARRAN1:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D")))) ")" ))) ; theorem :: REARRAN1:2 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_rearran1 :::"ascending"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) ")" )) ; theorem :: REARRAN1:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "D"))))) ; theorem :: REARRAN1:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: REARRAN1:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v2_rearran1 :::"ascending"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: REARRAN1:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v2_rearran1 :::"ascending"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: REARRAN1:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: REARRAN1:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: REARRAN1:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v3_rearran1 :::"lenght_equal_card_of_set"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: REARRAN1:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_rearran1 :::"terms've_same_card_as_number"::: ) ($#v2_rearran1 :::"ascending"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "D"))) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Const "D")); func :::"Co_Gen"::: "A" -> ($#m2_finseq_1 :::"RearrangmentGen":::) "of" "D" means :: REARRAN1:def 4 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "D" ($#k6_subset_1 :::"\"::: ) (Set "(" "A" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "A" ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ")" )))); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Const "D")) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Const "D")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Const "D")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ")" ))))) ; end; :: deftheorem defines :::"Co_Gen"::: REARRAN1:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "m")) ")" ) ")" )))) ")" ))); theorem :: REARRAN1:11 canceled; theorem :: REARRAN1:12 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" )))))) ; definitionlet "D", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Const "C")); let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Rland"::: "(" "F" "," "A" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: REARRAN1:def 5 (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" "F" "," "D" ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" "A" "," "C" ")" ")" ) ")" )); func :::"Rlor"::: "(" "F" "," "A" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: REARRAN1:def 6 (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" "F" "," "D" ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) "A" ")" ) "," "C" ")" ")" ) ")" )); end; :: deftheorem defines :::"Rland"::: REARRAN1:def 5 : (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" )))))); :: deftheorem defines :::"Rlor"::: REARRAN1:def 6 : (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ) "," (Set (Var "C")) ")" ")" ) ")" )))))); theorem :: REARRAN1:13 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: REARRAN1:14 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_rfinseq :::"MIM"::: ) (Set "(" (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) ")" ))) ")" ) ")" ))))) ; theorem :: REARRAN1:15 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ))))) ; theorem :: REARRAN1:16 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" )))))) ; theorem :: REARRAN1:17 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) "," (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; theorem :: REARRAN1:18 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ))))) ; theorem :: REARRAN1:19 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ))))) ; theorem :: REARRAN1:20 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:21 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "C")))))) ; theorem :: REARRAN1:22 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)))) "implies" (Bool (Set (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ))))) ; theorem :: REARRAN1:23 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ")" )))))) ; theorem :: REARRAN1:24 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) "," (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; theorem :: REARRAN1:25 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ))))) ; theorem :: REARRAN1:26 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "D")) ")" ))))) ; theorem :: REARRAN1:27 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:28 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) "," (Set ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" )) ")" )))) ; theorem :: REARRAN1:29 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) "," (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:30 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) "," (Set ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:31 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" ))) ")" )))) ; theorem :: REARRAN1:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: REARRAN1:33 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k3_rearran1 :::"Rland"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "A")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")))))))) ; theorem :: REARRAN1:34 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) "," (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:35 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))))) "holds" (Bool "(" (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) "," (Set ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) & (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) "," (Set (Var "D")) ")" )) ")" ))))) ; theorem :: REARRAN1:36 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" ))) ")" )))) ; theorem :: REARRAN1:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_rearran1 :::"Co_Gen"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: REARRAN1:38 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k4_rearran1 :::"Rlor"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "A")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")))))))) ; theorem :: REARRAN1:39 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"RearrangmentGen":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool "(" (Bool (Set ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) "," (Set (Var "F")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ) "," (Set (Var "F")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_rearran1 :::"Rland"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "F")))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k4_rearran1 :::"Rlor"::: ) "(" (Set (Var "F")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "F")))) ")" )))) ;