:: AFINSQ_2 semantic presentation begin theorem :: AFINSQ_2:1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )))) ; registration cluster ($#v7_ordinal1 :::"natural"::: ) -> ($#v6_membered :::"natural-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin theorem :: AFINSQ_2:2 (Bool "for" (Set (Var "X0")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "X0")) ($#r1_tarski :::"c="::: ) (Set (Var "n"))))) ; theorem :: AFINSQ_2:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: AFINSQ_2:4 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) "holds" (Bool (Set (Var "p")) "is" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D"))))) ; scheme :: AFINSQ_2:sch 1 XSeqLambdaD{ F1() -> ($#m1_hidden :::"Nat":::), F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "j")) ")" )) ")" ) ")" )) proof end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v1_finset_1 :::"finite"::: ) bbbadV1_AFINSQ_1() for ($#m1_hidden :::"set"::: ) ; let "p" be ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "p") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k35_valued_1 :::"""::: ) ) -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set ($#k54_valued_1 :::"|."::: ) "p" ($#k54_valued_1 :::".|"::: ) ) -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; let "q" be ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "p" ($#k1_valued_1 :::"+"::: ) "q") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k45_valued_1 :::"-"::: ) "q") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k18_valued_1 :::"(#)"::: ) "q") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k50_valued_1 :::"/""::: ) "q") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; end; registrationlet "p" be ($#v1_valued_0 :::"complex-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set ($#k54_valued_1 :::"|."::: ) "p" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; let "q" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "p" ($#k1_valued_1 :::"+"::: ) "q") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k45_valued_1 :::"-"::: ) "q") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k18_valued_1 :::"(#)"::: ) "q") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k50_valued_1 :::"/""::: ) "q") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "q" ($#k50_valued_1 :::"/""::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "p" be ($#v5_ordinal1 :::"T-Sequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "c" ($#k7_valued_1 :::"+"::: ) "p") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "p" ($#k13_valued_1 :::"-"::: ) "c") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; cluster (Set "c" ($#k24_valued_1 :::"(#)"::: ) "p") -> ($#v5_ordinal1 :::"T-Sequence-like"::: ) ; end; registrationlet "p" be ($#v1_valued_0 :::"complex-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "c" ($#k7_valued_1 :::"+"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "p" ($#k13_valued_1 :::"-"::: ) "c") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "c" ($#k24_valued_1 :::"(#)"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"XFinSequence":::); func :::"Rev"::: "p" -> ($#m1_hidden :::"XFinSequence":::) means :: AFINSQ_2:def 1 (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) "p" ")" ) ($#k21_binop_2 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Rev"::: AFINSQ_2:def 1 : (Bool "for" (Set (Var "p")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_2 :::"Rev"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k21_binop_2 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" )); theorem :: AFINSQ_2:5 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_afinsq_2 :::"Rev"::: ) (Set (Var "p")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_afinsq_2 :::"Rev"::: ) (Set (Var "p")) ")" ))) ")" )) ; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); cluster (Set ($#k1_afinsq_2 :::"Rev"::: ) "f") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"XFinSequence":::); let "n" be ($#m1_hidden :::"Nat":::); func "p" :::"/^"::: "n" -> ($#m1_hidden :::"XFinSequence":::) means :: AFINSQ_2:def 2 (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) "n")) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) "n" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"/^"::: AFINSQ_2:def 2 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" )))); theorem :: AFINSQ_2:6 (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 (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: AFINSQ_2:7 (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")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set (Var "n")))))) ; theorem :: AFINSQ_2:8 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k23_binop_2 :::"+"::: ) (Set (Var "n")) ")" ))))) ; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"XFinSequence":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k2_afinsq_2 :::"/^"::: ) "n") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: AFINSQ_2:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))))) ; theorem :: AFINSQ_2:10 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "p")))) ; theorem :: AFINSQ_2:11 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q")) ")" ) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "i")))))) ; theorem :: AFINSQ_2:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q")) ")" ) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: AFINSQ_2:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k2_afinsq_2 :::"/^"::: ) "n") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"XFinSequence":::); let "k1", "k2" be ($#m1_hidden :::"Nat":::); func :::"mid"::: "(" "p" "," "k1" "," "k2" ")" -> ($#m1_hidden :::"XFinSequence":::) equals :: AFINSQ_2:def 3 (Set (Set "(" "p" ($#k5_relat_1 :::"|"::: ) "k2" ")" ) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" "k1" ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"mid"::: AFINSQ_2:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set (Var "k2")) ")" ) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" (Set (Var "k1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))))); theorem :: AFINSQ_2:14 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k2")))) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: AFINSQ_2:15 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k1"))) & (Bool (Set (Var "k2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" (Set (Var "k1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "k2")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k1")) ")" ))))) ; theorem :: AFINSQ_2:16 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Num 1) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set (Var "k")))))) ; theorem :: AFINSQ_2:17 (Bool "for" (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_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Num 1) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: AFINSQ_2:18 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set (Var "p")) "," (Num 1) "," (Set (Var "k")) ")" )))) ; theorem :: AFINSQ_2:19 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k3_afinsq_2 :::"mid"::: ) "(" (Set "(" (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k23_binop_2 :::"+"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); let "k1", "k2" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k3_afinsq_2 :::"mid"::: ) "(" "f" "," "k1" "," "k2" ")" ) -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; begin definitionlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Sgm0"::: "X" -> ($#m1_hidden :::"XFinSequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: AFINSQ_2:def 4 (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) it)) & (Bool (Set (Var "k1")) ($#r1_hidden :::"="::: ) (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "l")))) & (Bool (Set (Var "k2")) ($#r1_hidden :::"="::: ) (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k2"))) ")" ) ")" ); end; :: deftheorem defines :::"Sgm0"::: AFINSQ_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_afinsq_2 :::"Sgm0"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "l")) "," (Set (Var "m")) "," (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "b2")))) & (Bool (Set (Var "k1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "l")))) & (Bool (Set (Var "k2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k2"))) ")" ) ")" ) ")" ))); registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_afinsq_2 :::"Sgm0"::: ) "A") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: AFINSQ_2:20 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) ; theorem :: AFINSQ_2:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set (Var "Y")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set (Var "X")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: AFINSQ_2:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; definitionlet "B1", "B2" be ($#m1_hidden :::"set"::: ) ; pred "B1" :::""::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_afinsq_2 :::""::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_afinsq_2 :::""::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_afinsq_2 :::" ($#m1_hidden :::"XFinSequence":::) equals :: AFINSQ_2:def 7 (Set "f" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set "(" "B" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) "f" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"SubXFinS"::: AFINSQ_2:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" (Set (Var "f")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ")" ))))); theorem :: AFINSQ_2:36 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k4_afinsq_2 :::"Sgm0"::: ) (Set "(" (Set (Var "B")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))) ; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"XFinSequence":::) "of" (Set (Const "D")); let "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" "f" "," "B" ")" ) -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" "p" "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_afinsq_2 :::"SubXFinS"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," "B" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; 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"::: ) ; end; scheme :: AFINSQ_2:sch 2 Sch5{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "F"))])) provided (Bool P1[(Set ($#k4_afinsq_1 :::"<%>"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "F"))])) "holds" (Bool P1[(Set (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "d")) ($#k5_afinsq_1 :::"%>"::: ) ))]))) proof end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"XFinSequence":::); assume (Bool (Set (Const "F")) "is" (Set (Const "D")) ($#v5_relat_1 :::"-valued"::: ) ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); assume (Bool "(" (Bool (Set (Const "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Const "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) ; func "b" :::""**""::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" "D" means :: AFINSQ_2:def 8 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "b")) if (Bool "(" (Bool "b" "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "D" "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) "F"))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "b" ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) "F" ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" ))) ")" )); end; :: deftheorem defines :::""**""::: AFINSQ_2:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "D")) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "b")))) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" "not" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ")" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F")) ")" ) ($#k21_binop_2 :::"-"::: ) (Num 1) ")" ))) ")" )) ")" ) ")" ")" ))))); theorem :: AFINSQ_2:37 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "d")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d")))))) ; theorem :: AFINSQ_2:38 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k6_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ))))) ; theorem :: AFINSQ_2:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "d")) "," (Set (Var "d1")) "," (Set (Var "d2")) ($#k7_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d1")) ")" ")" ) "," (Set (Var "d2")) ")" ))))) ; theorem :: AFINSQ_2:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "d")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")) ")" ) "," (Set (Var "d")) ")" )))))) ; theorem :: AFINSQ_2:41 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "G")) ")" ) ")" ))))) ; theorem :: AFINSQ_2:42 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")) ")" ) "," (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "G")) ")" ) ")" ))))) ; theorem :: AFINSQ_2:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))))))) ; theorem :: AFINSQ_2:44 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_finsop_1 :::""**""::: ) (Set "(" ($#k10_afinsq_1 :::"XFS2FS"::: ) (Set (Var "F")) ")" )))))) ; theorem :: AFINSQ_2:45 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "b")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "b")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "G")))))))) ; theorem :: AFINSQ_2:46 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "bFG")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "b")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "or" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" ) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "bFG")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "bFG"))))) "holds" (Bool (Set (Set (Var "bFG")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set "(" (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "bFG")))))))) ; theorem :: AFINSQ_2:47 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D2")) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "D1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "D2")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Set (Var "b1")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "b1")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))))))) ; definitionlet "F" be ($#m1_hidden :::"XFinSequence":::); func :::"Sum"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: AFINSQ_2:def 9 (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k6_afinsq_2 :::""**""::: ) "F"); end; :: deftheorem defines :::"Sum"::: AFINSQ_2:def 9 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k27_binop_2 :::"addcomplex"::: ) ) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))); registrationlet "f" be ($#v1_xboole_0 :::"empty"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k7_afinsq_2 :::"Sum"::: ) "f") -> ($#v1_xboole_0 :::"zero"::: ) ; end; theorem :: AFINSQ_2:48 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_valued_0 :::"real-valued"::: ) )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))) ; theorem :: AFINSQ_2:49 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k39_binop_2 :::"addrat"::: ) ) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))) ; theorem :: AFINSQ_2:50 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k44_binop_2 :::"addint"::: ) ) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))) ; theorem :: AFINSQ_2:51 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_valued_0 :::"natural-valued"::: ) )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k47_binop_2 :::"addnat"::: ) ) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F"))))) ; registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k7_afinsq_2 :::"Sum"::: ) "F") -> ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "F" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k7_afinsq_2 :::"Sum"::: ) "F") -> ($#v1_rat_1 :::"rational"::: ) ; end; registrationlet "F" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k7_afinsq_2 :::"Sum"::: ) "F") -> ($#v1_int_1 :::"integer"::: ) ; end; registrationlet "F" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"XFinSequence":::); cluster (Set ($#k7_afinsq_2 :::"Sum"::: ) "F") -> ($#v7_ordinal1 :::"natural"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v4_valued_0 :::"natural-valued"::: ) -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: AFINSQ_2:52 (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "cF")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: AFINSQ_2:53 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "c")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "c")))) ; theorem :: AFINSQ_2:54 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k6_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "c2"))))) ; theorem :: AFINSQ_2:55 (Bool "for" (Set (Var "cF1")) "," (Set (Var "cF2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" (Set (Var "cF1")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "cF2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF1")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF2")) ")" )))) ; theorem :: AFINSQ_2:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "rF")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "rF")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "S")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: AFINSQ_2:57 (Bool "for" (Set (Var "rF1")) "," (Set (Var "rF2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "rF1"))))) "holds" (Bool (Set (Set (Var "rF1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "rF2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF2"))))) ; theorem :: AFINSQ_2:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" (Set (Var "n")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_binop_2 :::"*"::: ) (Set (Var "c")))))) ; theorem :: AFINSQ_2:59 (Bool "for" (Set (Var "rF")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "rF"))))) "holds" (Bool (Set (Set (Var "rF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "r")))))) ; theorem :: AFINSQ_2:60 (Bool "for" (Set (Var "rF")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "rF"))))) "holds" (Bool (Set (Set (Var "rF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "r")))))) ; theorem :: AFINSQ_2:61 (Bool "for" (Set (Var "rF")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "rF")) "is" ($#v4_partfun3 :::"nonnegative-yielding"::: ) ) & (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "rF")))) & (Bool (Set (Set (Var "rF")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))) ; theorem :: AFINSQ_2:62 (Bool "for" (Set (Var "rF")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "rF")) "is" ($#v4_partfun3 :::"nonnegative-yielding"::: ) )) "holds" (Bool "(" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "rF"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "rF")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "rF")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ) ")" )) ; theorem :: AFINSQ_2:63 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "cF")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "cF")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "n"))))))) ; theorem :: AFINSQ_2:64 (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "c")) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "cF")) ")" ))))) ; theorem :: AFINSQ_2:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "cF"))))) "holds" (Bool (Set (Set "(" ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" (Set (Var "cF")) ($#k5_relat_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "cF")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" (Set (Var "cF")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "n")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: AFINSQ_2:66 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: AFINSQ_2:67 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: AFINSQ_2:68 (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "cF"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k5_binop_2 :::"*"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "cF")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "c")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))))) ; theorem :: AFINSQ_2:69 (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set (Var "cF"))) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_2 :::"Sum"::: ) (Set "(" ($#k1_afinsq_2 :::"Rev"::: ) (Set (Var "cF")) ")" )))) ; theorem :: AFINSQ_2:70 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "fp")) "," (Set (Var "fq")) "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")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "fp")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p")))) & (Bool (Set (Var "fq")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "fq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q")) ")" ))))) ; theorem :: AFINSQ_2:71 (Bool "for" (Set (Var "cF")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"XFinSequence":::) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B1")) ($#r1_afinsq_2 :::""::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "b")))))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"XFinSequence":::) "of" (Set (Set (Const "D")) ($#k8_afinsq_1 :::"^omega"::: ) ); func :::"FlattenSeq"::: "F" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "D" ($#k8_afinsq_1 :::"^omega"::: ) ) means :: AFINSQ_2:def 10 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "D" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "D" ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k15_afinsq_1 :::"^"::: ) (Set (Var "q")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_afinsq_2 :::""**""::: ) "F")) ")" )); end; :: deftheorem defines :::"FlattenSeq"::: AFINSQ_2:def 10 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k15_afinsq_1 :::"^"::: ) (Set (Var "q")))) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k6_afinsq_2 :::""**""::: ) (Set (Var "F")))) ")" )) ")" )))); theorem :: AFINSQ_2:73 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "d")) ($#k5_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ; theorem :: AFINSQ_2:74 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set "(" ($#k4_afinsq_1 :::"<%>"::: ) (Set "(" (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_afinsq_1 :::"<%>"::: ) (Set (Var "D"))))) ; theorem :: AFINSQ_2:75 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set "(" (Set (Var "F")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "F")) ")" ) ($#k15_afinsq_1 :::"^"::: ) (Set "(" ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "G")) ")" ))))) ; theorem :: AFINSQ_2:76 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k6_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k15_afinsq_1 :::"^"::: ) (Set (Var "q")))))) ; theorem :: AFINSQ_2:77 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set ($#k7_afinsq_1 :::"<%"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k7_afinsq_1 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k15_afinsq_1 :::"^"::: ) (Set (Var "q")) ")" ) ($#k15_afinsq_1 :::"^"::: ) (Set (Var "r")))))) ; theorem :: AFINSQ_2:78 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set "(" (Set (Var "q")) ($#k2_afinsq_2 :::"/^"::: ) (Set "(" ($#k1_afinsq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: AFINSQ_2:79 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) ; theorem :: AFINSQ_2:80 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "q")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; theorem :: AFINSQ_2:81 (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"XFinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set (Var "r"))))) ; theorem :: AFINSQ_2:82 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"XFinSequence":::) "of" (Set (Set (Var "D")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_afinsq_2 :::"FlattenSeq"::: ) (Set (Var "G")))))) ; registrationlet "p" be ($#m1_hidden :::"XFinSequence":::); let "q" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"XFinSequence":::); cluster (Set "p" ($#k1_ordinal4 :::"^"::: ) "q") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "q" ($#k1_ordinal4 :::"^"::: ) "p") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: AFINSQ_2:83 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"XFinSequence":::) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set "(" (Set (Var "p")) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ;