:: RFINSEQ  semantic presentation begin  











registrationlet "f" be   ($#m1_hidden :::"FinSequence":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k10_relat_1 :::"Coim"::: )   "(" "f" "," "x" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: RFINSEQ:1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) "iff" (Bool (Set (Set (Var "f"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "h"))) "," (Set (Set (Var "g"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "h")))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )  ")" )) ; 
 
theorem :: RFINSEQ:2 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g"))) "," (Set (Set (Var "g"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f")))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) ; 
 
theorem :: RFINSEQ:3 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "g")))) & (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "g"))))  ")" )) ; 
 
theorem :: RFINSEQ:4 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) "iff" (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "g")) ")" ) "st" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "P")))))  ")" )) ; 
 
theorem :: RFINSEQ:5 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "," (Set (Var "f"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#m1_hidden :::"FinSequence":::); func "f" :::"/^"::: "n" ->   ($#m1_hidden :::"FinSequence":::) means :: RFINSEQ:def 1 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  "f" ")" )  ($#k9_real_1 :::"-"::: )  "n")) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  "n" ")" )))  ")" )  ")" ) if (Bool "n"  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f"))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 






:: deftheorem    defines :::"/^"::: RFINSEQ:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_rfinseq :::"/^"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "n")))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" )))  ")" )  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_rfinseq :::"/^"::: )  (Set (Var "n")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")"   ")" ))); 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); let "f" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); :: original: :::"/^"::: redefine func "f" :::"/^"::: "n" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D"; end; 
theorem :: RFINSEQ:6 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))  ")" )))) ; 
 
theorem :: RFINSEQ:7 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; 
 
theorem :: RFINSEQ:8 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "f"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f")))))) ; 
 
theorem :: RFINSEQ:9 (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "R1")) "," (Set (Var "R2"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "R1")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "R2"))))) ; 
 definitionlet "R" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); func  :::"MIM"::: "R" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: RFINSEQ:def 2 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "R")) & (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  it ")" ))  ($#r1_hidden :::"="::: )  (Set "R"  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  "R" ")" ))) & (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_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "R"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" "R"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"MIM"::: RFINSEQ:def 2 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "b2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))) & (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")) ")" ))) & (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 "b2")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" )); 
 
theorem :: RFINSEQ:10 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 2))) & (Bool (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k3_rfinseq :::"MIM"::: )  (Set  "(" (Set (Var "R"))  ($#k17_finseq_1 :::"|"::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: RFINSEQ:11 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 2))) & (Bool (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) "," (Set (Var "s")) ($#k2_finseq_4 :::"*>"::: ) )))))) ; 
 
theorem :: RFINSEQ:12 (Bool (Set   ($#k3_rfinseq :::"MIM"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))) ; 
 
theorem :: RFINSEQ:13 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k3_rfinseq :::"MIM"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: RFINSEQ:14 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set   ($#k3_rfinseq :::"MIM"::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k2_finseq_4 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_finseq_4 :::"<*"::: ) (Set  "(" (Set (Var "r"))  ($#k9_real_1 :::"-"::: )  (Set (Var "s")) ")" ) "," (Set (Var "s")) ($#k2_finseq_4 :::"*>"::: ) ))) ; 
 
theorem :: RFINSEQ:15 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")) ")" )  ($#k2_rfinseq :::"/^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_rfinseq :::"MIM"::: )  (Set  "(" (Set (Var "R"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: RFINSEQ:16 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k3_rfinseq :::"MIM"::: )  (Set (Var "R")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Num 1)))) ; 
 
theorem :: RFINSEQ:17 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R"))))) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k3_rfinseq :::"MIM"::: )  (Set  "(" (Set (Var "R"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))))) ; 
 definitionlet "IT" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); redefine attr "IT" is  :::"non-increasing":::  means :: RFINSEQ:def 3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "IT")) & (Bool (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "IT"))) "holds"  (Bool (Set "IT"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set "IT"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )))); end; 




:: deftheorem    defines :::"non-increasing"::: RFINSEQ:def 3 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "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 "IT")))) & (Bool (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "IT"))))) "holds"  (Bool (Set (Set (Var "IT"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "IT"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )   bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0()   ($#v8_valued_0 :::"non-increasing"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ); 
end; 
theorem :: RFINSEQ:18 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) "holds"  (Bool (Set (Var "R")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  )) ; 
 
theorem :: RFINSEQ:19 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) "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"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "R")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "R")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "R"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))))  ")" )) ; 
 
theorem :: RFINSEQ:20 (Bool  "for" (Set (Var "R")) "being"   ($#v8_valued_0 :::"non-increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "R"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "n"))) "is"   ($#v8_valued_0 :::"non-increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )))) ; 
 
theorem :: RFINSEQ:21 (Bool  "for" (Set (Var "R")) "being"   ($#v8_valued_0 :::"non-increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "R"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "n"))) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ))) ; 
 
theorem :: RFINSEQ:22 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) (Bool  "ex" (Set (Var "R1")) "being"   ($#v8_valued_0 :::"non-increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st" (Bool (Set (Var "R")) "," (Set (Var "R1"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ))) ; 
 
theorem :: RFINSEQ:23 (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being"   ($#v8_valued_0 :::"non-increasing"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "R1")) "," (Set (Var "R2"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) "holds"  (Bool (Set (Var "R1"))  ($#r1_hidden :::"="::: )  (Set (Var "R2")))) ; 
 
theorem :: RFINSEQ:24 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "R"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "s"))  ($#k10_real_1 :::"/"::: )  (Set (Var "r")) ")" ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "R")) ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: RFINSEQ:25 (Bool  "for" (Set (Var "R")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "R")) ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "R"))))) ; 
 begin  




theorem :: RFINSEQ:26 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) ; 
 
theorem :: RFINSEQ:27 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_rfinseq :::"/^"::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: RFINSEQ:28 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ))) ; 
 
theorem :: RFINSEQ:29 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "f"))  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )  ($#k1_xreal_0 :::"-'"::: )  (Set (Var "k"))))))) ; 
 
theorem :: RFINSEQ:30 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: RFINSEQ:31 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) "iff" (Bool (Set (Set (Var "h"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f"))) "," (Set (Set (Var "h"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "g")))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )  ")" )) ; 
 
theorem :: RFINSEQ:32 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )))) ; 
 
theorem :: RFINSEQ:33 (Bool  "for" (Set (Var "t")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) (Bool  "ex" (Set (Var "u")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "t")) "," (Set (Var "u"))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  ) & (Bool (Set (Var "u")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  )) & (Bool (Set (Var "u")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  )  ")" ))) ;