:: AFINSQ_1  semantic presentation begin  

















theorem :: AFINSQ_1:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) ; 
 
theorem :: AFINSQ_1:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: AFINSQ_1:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: AFINSQ_1:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )))) ; 
 
theorem :: AFINSQ_1:5 (Bool  "for" (Set (Var "r")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "r")) "is"   ($#v5_ordinal1 :::"T-Sequence-like"::: )  )  ")" ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))  ")" )) ; 
 definitionmode XFinSequence is   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"T-Sequence":::); end; 






registrationlet "p" be   ($#m1_hidden :::"XFinSequence":::); 
cluster (Set   ($#k9_xtuple_0 :::"dom"::: )  "p") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; notationlet "p" be   ($#m1_hidden :::"XFinSequence":::); synonym  :::"len"::: "p" for  :::"card"::: "p"; end; registrationlet "p" be   ($#m1_hidden :::"XFinSequence":::); 
identify ; 
end; definitionlet "p" be   ($#m1_hidden :::"XFinSequence":::); :: original: :::"len"::: redefine func  :::"len"::: "p" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "p" be   ($#m1_hidden :::"XFinSequence":::); :: original: :::"dom"::: redefine func  :::"dom"::: "p" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); end; 
theorem :: AFINSQ_1:6 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "k"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "p"))))) ; 
 scheme  :: AFINSQ_1:sch 1 XSeqEx{ F1() ->   ($#m1_hidden :::"Nat":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "k")) "," (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))])  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "k")) "," (Set (Var "x"))])))
 proof 


end; scheme  :: AFINSQ_1:sch 2 XSeqLambda{ F1() ->   ($#m1_hidden :::"Nat":::), F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "k")) ")" ))  ")" )  ")" ))
 proof 


end; 
theorem :: AFINSQ_1:7 (Bool  "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")" )))) ; 
 
theorem :: AFINSQ_1:8 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: AFINSQ_1:9 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 registrationlet "p" be   ($#m1_hidden :::"XFinSequence":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "p"  ($#k5_relat_1 :::"|"::: )  "n") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: AFINSQ_1:10 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "p"))) "is"   ($#m1_hidden :::"XFinSequence":::)))) ; 
 
theorem :: AFINSQ_1:11 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k"))))) ; 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; mode XFinSequence of "D" is   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"T-Sequence":::) "of" "D"; end; 
theorem :: AFINSQ_1:12 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D"))))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_xboole_0 :::"empty"::: )    ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 



theorem :: AFINSQ_1:13 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "k"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "a"))) "is"   ($#m1_hidden :::"XFinSequence":::)))) ; 
 
theorem :: AFINSQ_1:14 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "st" (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))))) ; 
 
theorem :: AFINSQ_1:15 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: AFINSQ_1:16 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))) ; 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_xboole_0 :::"empty"::: )     ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "x" be    ($#m1_hidden :::"set"::: )  ; func :::"<%":::"x":::"%>"::: ->    ($#m1_hidden :::"set"::: )   equals :: AFINSQ_1:def 1 (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  "x"); end; 





:: deftheorem    defines :::"<%"::: AFINSQ_1:def 1 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k3_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k3_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "x"))))); 
 registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "x" ($#k3_afinsq_1 :::"%>"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; func  :::"<%>"::: "D" ->   ($#m1_hidden :::"XFinSequence":::) "of" "D" equals :: AFINSQ_1:def 2 (Set   ($#k1_xboole_0 :::"{}"::: )  ); end; 





:: deftheorem    defines :::"<%>"::: AFINSQ_1:def 2 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_afinsq_1 :::"<%>"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))); 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_afinsq_1 :::"<%>"::: )  "D") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; definitionlet "p", "q" be   ($#m1_hidden :::"XFinSequence":::); redefine func "p" :::"^"::: "q" means :: AFINSQ_1:def 3 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  "p" ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  "q" ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  "p"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  "q"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  "p" ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set "q"  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"^"::: AFINSQ_1:def 3 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )  ")" )  ")" ))); 
 registrationlet "p", "q" be   ($#m1_hidden :::"XFinSequence":::); 
cluster (Set "p"  ($#k1_ordinal4 :::"^"::: )  "q") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: AFINSQ_1:17 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: AFINSQ_1:18 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")" ))))) ; 
 
theorem :: AFINSQ_1:19 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" ) ")" ))))) ; 
 
theorem :: AFINSQ_1:20 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ))) "or" (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))) "or" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "q")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "n"))))  ")" ))  ")" ))) ; 
 
theorem :: AFINSQ_1:21 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "p")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: AFINSQ_1:22 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )))  ")" )))) ; 
 
theorem :: AFINSQ_1:23 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: AFINSQ_1:24 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: AFINSQ_1:25 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "q")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: AFINSQ_1:26 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: AFINSQ_1:27 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set  "(" (Set (Var "q"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: AFINSQ_1:28 (Bool  "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "r")))) "or" (Bool (Set (Set (Var "r"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))))  ")" )) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 registrationlet "p" be   ($#m1_hidden :::"XFinSequence":::); 
reduce ; 

reduce ; 
end; 
theorem :: AFINSQ_1:29 canceled; 
 
theorem :: AFINSQ_1:30 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; let "p", "q" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); 
cluster (Set "p"  ($#k1_ordinal4 :::"^"::: )  "q") -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; definitionlet "x" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"<%"::: redefine func :::"<%":::"x":::"%>"::: ->   ($#m1_hidden :::"Function":::) means :: AFINSQ_1:def 4 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "x")  ")" ); end; 





:: deftheorem    defines :::"<%"::: AFINSQ_1:def 4 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" ))); 
 registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "x" ($#k3_afinsq_1 :::"%>"::: ) ) ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "x" ($#k3_afinsq_1 :::"%>"::: ) ) ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: AFINSQ_1:31 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))) "holds"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D"))) & (Bool (Set (Var "q")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))  ")" ))) ; 
 definitionlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; func :::"<%":::"x" "," "y":::"%>"::: ->    ($#m1_hidden :::"set"::: )   equals :: AFINSQ_1:def 5 (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) "x" ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "y" ($#k5_afinsq_1 :::"%>"::: ) )); let "z" be    ($#m1_hidden :::"set"::: )  ; func :::"<%":::"x" "," "y" "," "z":::"%>"::: ->    ($#m1_hidden :::"set"::: )   equals :: AFINSQ_1:def 6 (Set (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) "x" ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "y" ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "z" ($#k5_afinsq_1 :::"%>"::: ) )); end; 













:: deftheorem    defines :::"<%"::: AFINSQ_1:def 5 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k6_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "y")) ($#k5_afinsq_1 :::"%>"::: ) )))); 
 
:: deftheorem    defines :::"<%"::: AFINSQ_1:def 6 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k7_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "y")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "z")) ($#k5_afinsq_1 :::"%>"::: ) )))); 
 registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k6_afinsq_1 :::"<%"::: ) "x" "," "y" ($#k6_afinsq_1 :::"%>"::: ) ) ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
let "z" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k7_afinsq_1 :::"<%"::: ) "x" "," "y" "," "z" ($#k7_afinsq_1 :::"%>"::: ) ) ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k6_afinsq_1 :::"<%"::: ) "x" "," "y" ($#k6_afinsq_1 :::"%>"::: ) ) ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
let "z" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k7_afinsq_1 :::"<%"::: ) "x" "," "y" "," "z" ($#k7_afinsq_1 :::"%>"::: ) ) ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: AFINSQ_1:32 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: AFINSQ_1:33 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: AFINSQ_1:34 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" ))) ; 
 
theorem :: AFINSQ_1:35 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: AFINSQ_1:36 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: AFINSQ_1:37 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k7_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k6_afinsq_1 :::"%>"::: ) ))) & (Bool (Set  ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k7_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k6_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "z")) ($#k5_afinsq_1 :::"%>"::: ) )))  ")" )) ; 
 
theorem :: AFINSQ_1:38 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k6_afinsq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )  ")" ))) ; 
 
theorem :: AFINSQ_1:39 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k7_afinsq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 3)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "z")))  ")" )  ")" ))) ; 
 registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "x" ($#k3_afinsq_1 :::"%>"::: ) ) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
let "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k6_afinsq_1 :::"<%"::: ) "x" "," "y" ($#k6_afinsq_1 :::"%>"::: ) ) -> (Num 2)  ($#v3_card_1 :::"-element"::: )   ; 
let "z" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k7_afinsq_1 :::"<%"::: ) "x" "," "y" "," "z" ($#k7_afinsq_1 :::"%>"::: ) ) -> (Num 3)  ($#v3_card_1 :::"-element"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )   "n"  ($#v3_card_1 :::"-element"::: )    -> "n"  ($#v4_relat_1 :::"-defined"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "n"  ($#k2_funcop_1 :::"-->"::: )  "x") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )   "n"  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "n"  ($#v4_relat_1 :::"-defined"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )   "n"  ($#v3_card_1 :::"-element"::: )    -> "n"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_partfun1 :::"total"::: )   "n"  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: AFINSQ_1:40 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)(Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )))))) ; 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "d1" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "d1" ($#k3_afinsq_1 :::"%>"::: ) ) -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
let "d2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); 
cluster (Set  ($#k6_afinsq_1 :::"<%"::: ) "d1" "," "d2" ($#k6_afinsq_1 :::"%>"::: ) ) -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
let "d3" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); 
cluster (Set  ($#k7_afinsq_1 :::"<%"::: ) "d1" "," "d2" "," "d3" ($#k7_afinsq_1 :::"%>"::: ) ) -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; scheme  :: AFINSQ_1:sch 3 IndXSeq{ P1[  ($#m1_hidden :::"XFinSequence":::)] } : 
(Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool P1[(Set (Var "p"))]))
 provided
(Bool P1[(Set   ($#k1_xboole_0 :::"{}"::: )  )])
 and  
(Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "p"))])) "holds"  (Bool P1[(Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ))])))
 proof 


end; 
theorem :: AFINSQ_1:41 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "s")))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "r"))))) "holds"  (Bool  "ex" (Set (Var "t")) "being"   ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Var "r"))))) ; 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; func "D" :::"^omega":::  ->    ($#m1_hidden :::"set"::: )   means :: AFINSQ_1:def 7 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" "D")  ")" )); end; 





:: deftheorem    defines :::"^omega"::: AFINSQ_1:def 7 :  (Bool  "for" (Set (Var "D")) "," (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "D"))  ($#k8_afinsq_1 :::"^omega"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))  ")" ))  ")" )); 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: AFINSQ_1:42 (Bool  "for" (Set (Var "x")) "," (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "D"))  ($#k8_afinsq_1 :::"^omega"::: )  )) "iff" (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))  ")" )) ; 
 
theorem :: AFINSQ_1:43 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "D"))  ($#k8_afinsq_1 :::"^omega"::: )  ))) ; 
 scheme  :: AFINSQ_1:sch 4 SepXSeq{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[  ($#m1_hidden :::"XFinSequence":::)] } : 
(Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set F1 "("  ")" )  ($#k8_afinsq_1 :::"^omega"::: )  )) & (Bool P1[(Set (Var "p"))]) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" ))  ")" )))
 proof 


end; notationlet "p" be   ($#m1_hidden :::"XFinSequence":::); let "i", "x" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"Replace":::  "(" "p" "," "i" "," "x" ")"  for "p" :::"+*":::  "(" "i" "," "x" ")" ; end; registrationlet "p" be   ($#m1_hidden :::"XFinSequence":::); let "i", "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_funct_7 :::"Replace"::: )   "(" "p" "," "i" "," "x" ")" ) ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: AFINSQ_1:44 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "("  ($#k2_funct_7 :::"Replace"::: )   "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "x")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))) &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "implies" (Bool (Set (Set  "("  ($#k2_funct_7 :::"Replace"::: )   "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "x")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"  & (Bool  "("   "for" (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i")))) "holds"  (Bool (Set (Set  "("  ($#k2_funct_7 :::"Replace"::: )   "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "x")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))  ")" )  ")" )))) ; 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "p" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); let "i" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "D")); 
cluster (Set   ($#k2_funct_7 :::"Replace"::: )   "(" "p" "," "i" "," "a" ")" ) -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )    ->   ($#v3_valued_0 :::"real-valued"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )    ->   ($#v4_valued_0 :::"natural-valued"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: AFINSQ_1:45 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 4)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4")))  ")" ))) ; 
 
theorem :: AFINSQ_1:46 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x5")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 5)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "x5")))  ")" ))) ; 
 
theorem :: AFINSQ_1:47 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x5")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x6")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 6)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "x5"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Set (Var "x6")))  ")" ))) ; 
 
theorem :: AFINSQ_1:48 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x5")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x6")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x7")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 7)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "x5"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Set (Var "x6"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 6))  ($#r1_hidden :::"="::: )  (Set (Var "x7")))  ")" ))) ; 
 
theorem :: AFINSQ_1:49 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x5")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x6")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x7")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x8")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 8)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "x5"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Set (Var "x6"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 6))  ($#r1_hidden :::"="::: )  (Set (Var "x7"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 7))  ($#r1_hidden :::"="::: )  (Set (Var "x8")))  ")" ))) ; 
 
theorem :: AFINSQ_1:50 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "," (Set (Var "x9")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x5")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x6")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x7")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x8")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x9")) ($#k5_afinsq_1 :::"%>"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 9)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Var "x5"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Set (Var "x6"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 6))  ($#r1_hidden :::"="::: )  (Set (Var "x7"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 7))  ($#r1_hidden :::"="::: )  (Set (Var "x8"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 8))  ($#r1_hidden :::"="::: )  (Set (Var "x9")))  ")" ))) ; 
 
theorem :: AFINSQ_1:51 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: AFINSQ_1:52 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))) ; 
 
theorem :: AFINSQ_1:53 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: AFINSQ_1:54 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))) ; 
 
theorem :: AFINSQ_1:55 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))))) ; 
 
theorem :: AFINSQ_1:56 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))))) ; 
 
theorem :: AFINSQ_1:57 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: AFINSQ_1:58 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")))))) ; 
 
theorem :: AFINSQ_1:59 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set  "(" (Set (Var "q"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: AFINSQ_1:60 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "n")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))))))) ; 
 
theorem :: AFINSQ_1:61 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k"))))) "holds"  (Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_hidden :::"XFinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q1")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q2")))  ($#r1_hidden :::"="::: )  (Set (Var "k"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q1"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q2"))))  ")" )))) ; 
 
theorem :: AFINSQ_1:62 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  "st" (Bool (Bool (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "y")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ))) ; 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); func  :::"FS2XFS"::: "q" ->   ($#m1_hidden :::"XFinSequence":::) "of" "D" means :: AFINSQ_1:def 8 (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "q")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "q"))) "holds"  (Bool (Set "q"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"FS2XFS"::: AFINSQ_1:def 8 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_afinsq_1 :::"FS2XFS"::: )  (Set (Var "q")))) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" )  ")" )))); 
 


definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "q" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); func  :::"XFS2FS"::: "q" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D" means :: AFINSQ_1:def 9 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  "q")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  "q"))) "holds"  (Bool (Set "q"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"XFS2FS"::: AFINSQ_1:def 9 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_afinsq_1 :::"XFS2FS"::: )  (Set (Var "q")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" )  ")" )))); 
 
theorem :: AFINSQ_1:63 (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "r"))) "is"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); let "n" be   ($#m1_hidden :::"Nat":::); assume that  
(Bool (Set (Const "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Const "q"))))
 and  
(Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Const "D")))
 ; func  :::"FS2XFS*":::  "(" "q" "," "n" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of" "D" means :: AFINSQ_1:def 10 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "q")  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  "n") & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "q"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "q"  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "q")  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  "n")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" ); end; 








:: deftheorem    defines :::"FS2XFS*"::: AFINSQ_1:def 10 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))) & (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "D")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_afinsq_1 :::"FS2XFS*"::: )   "(" (Set (Var "q")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool  "("   "for" (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" ))))); 
 





definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "p" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); assume that  
(Bool (Set (Set (Const "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::))
 and  
(Bool (Set (Set (Const "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Const "p"))))
 ; func  :::"XFS2FS*"::: "p" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" "D" means :: AFINSQ_1:def 11 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"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 it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" )); end; 







:: deftheorem    defines :::"XFS2FS*"::: AFINSQ_1:def 11 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"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 "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" ))  ")" )))); 
 
theorem :: AFINSQ_1:64 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 definitionlet "F" be   ($#m1_hidden :::"Function":::); attr "F" is  :::"initial":::  means :: AFINSQ_1:def 12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "F")) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "F"))); end; 




:: deftheorem    defines :::"initial"::: AFINSQ_1:def 12 :  (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_afinsq_1 :::"initial"::: )  ) "iff" (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_afinsq_1 :::"initial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )    ->   ($#v1_afinsq_1 :::"initial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )    -> (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: AFINSQ_1:65 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: AFINSQ_1:66 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "F")))) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "F"))))  ")" ))) ; 
 
theorem :: AFINSQ_1:67 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "G")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Var "G")) "is"   ($#v1_afinsq_1 :::"initial"::: )  ))) ; 
 
theorem :: AFINSQ_1:68 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "F"))))  "}"  )) ; 
 
theorem :: AFINSQ_1:69 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "G")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r1_tarski :::"c="::: )  (Set (Var "G"))) & (Bool (Set   ($#k62_valued_1 :::"LastLoc"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k62_valued_1 :::"LastLoc"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "G"))))) ; 
 
theorem :: AFINSQ_1:70 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k62_valued_1 :::"LastLoc"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "F")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1)))) ; 
 
theorem :: AFINSQ_1:71 (Bool  "for" (Set (Var "F")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k64_valued_1 :::"FirstLoc"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "F" be (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k63_valued_1 :::"CutLastLoc"::: )  "F") ->   ($#v1_afinsq_1 :::"initial"::: )   ; 
end; 



theorem :: AFINSQ_1:72 (Bool  "for" (Set (Var "I")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "I")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "J")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" ) ")"  ")" ))))) ; 
 
theorem :: AFINSQ_1:73 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p")))))) "holds"  (Bool  "not" (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "m")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_afinsq_1 :::"dom"::: )  (Set (Var "p"))))))) ; 
 registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ) ->   ($#v4_funct_1 :::"functional"::: )   ; 
end; registrationlet "D" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ); 
end; definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); func  :::"Down"::: "f" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ) equals :: AFINSQ_1:def 13 "f"; end; 






:: deftheorem    defines :::"Down"::: AFINSQ_1:def 13 :  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "holds"  (Bool (Set   ($#k13_afinsq_1 :::"Down"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))); 
 definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); let "g" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set (Const "D"))  ($#k8_afinsq_1 :::"^omega"::: )  ); :: original: :::"^"::: redefine func "f" :::"^"::: "g" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ); end; definitionlet "D" be    ($#m1_hidden :::"set"::: )  ; let "f", "g" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set (Const "D"))  ($#k8_afinsq_1 :::"^omega"::: )  ); :: original: :::"^"::: redefine func "f" :::"^"::: "g" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set "D"  ($#k8_afinsq_1 :::"^omega"::: )  ); end; 
theorem :: AFINSQ_1:74 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Var "p"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))))) ; 
 
theorem :: AFINSQ_1:75 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: AFINSQ_1:76 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k6_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ; 
 



theorem :: AFINSQ_1:77 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "q")) "," (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "p")) ")" ) ")"  ")" )))) ; 
 
theorem :: AFINSQ_1:78 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")))) & (Bool (Set (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q"))))  ")" )) ; 
 




theorem :: AFINSQ_1:79 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "I")) "being" (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "J")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "I")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "J")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "I")) ")" ) ")" ) ")"  ")" )))))) ; 
 
theorem :: AFINSQ_1:80 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "p")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: AFINSQ_1:81 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "q")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: AFINSQ_1:82 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "p")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 
theorem :: AFINSQ_1:83 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"XFinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set  "(" (Set (Var "p"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "q")) ")" ) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k61_valued_1 :::"Shift"::: )   "(" (Set (Var "q")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "p")) ")" ) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))))) ; 
 registrationlet "F" be (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_afinsq_1 :::"initial"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k63_valued_1 :::"CutLastLoc"::: )  "F") ->   ($#v1_afinsq_1 :::"initial"::: )   ; 
end; definitionlet "x1", "x2", "x3", "x4" be    ($#m1_hidden :::"set"::: )  ; func :::"<%":::"x1" "," "x2" "," "x3" "," "x4":::"%>"::: ->    ($#m1_hidden :::"set"::: )   equals :: AFINSQ_1:def 14 (Set (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) "x1" ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "x2" ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "x3" ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) "x4" ($#k5_afinsq_1 :::"%>"::: ) )); end; 








:: deftheorem    defines :::"<%"::: AFINSQ_1:def 14 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x1")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x2")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x3")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x4")) ($#k5_afinsq_1 :::"%>"::: ) )))); 
 registrationlet "x1", "x2", "x3", "x4" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k16_afinsq_1 :::"<%"::: ) "x1" "," "x2" "," "x3" "," "x4" ($#k16_afinsq_1 :::"%>"::: ) ) ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; registrationlet "x1", "x2", "x3", "x4" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k16_afinsq_1 :::"<%"::: ) "x1" "," "x2" "," "x3" "," "x4" ($#k16_afinsq_1 :::"%>"::: ) ) ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; 






theorem :: AFINSQ_1:84 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) ))  ($#r1_hidden :::"="::: )  (Num 4))) ; 
 
theorem :: AFINSQ_1:85 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) )  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "x3"))) & (Bool (Set (Set  ($#k16_afinsq_1 :::"<%"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k16_afinsq_1 :::"%>"::: ) )  ($#k1_funct_1 :::"."::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Var "x4")))  ")" )) ;