:: FINSEQ_2 semantic presentation begin theorem :: FINSEQ_2:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) ; theorem :: FINSEQ_2:2 (Bool "for" (Set (Var "l")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l"))))) ; theorem :: FINSEQ_2:3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: FINSEQ_2:4 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j"))))) ; theorem :: FINSEQ_2:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: FINSEQ_2:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "i")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" )) ; theorem :: FINSEQ_2:7 (Bool "for" (Set (Var "i")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "l")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) "or" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l")))) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k1_nat_1 :::"+"::: ) (Num 1))) ")" )) ; theorem :: FINSEQ_2:8 (Bool "for" (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "l")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" )))) ; theorem :: FINSEQ_2:9 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: FINSEQ_2:10 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ; theorem :: FINSEQ_2:11 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "D")))))) ; theorem :: FINSEQ_2:12 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_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" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))))) ; theorem :: FINSEQ_2:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))))) ; theorem :: FINSEQ_2:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))))) ; theorem :: FINSEQ_2:15 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ))))) ; theorem :: FINSEQ_2:16 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: FINSEQ_2:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: FINSEQ_2:18 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::)(Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:19 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A"))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k9_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:20 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) ; theorem :: FINSEQ_2:21 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "i")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )))) ; theorem :: FINSEQ_2:22 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" )))) ; theorem :: FINSEQ_2:23 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ))))) ; scheme :: FINSEQ_2:sch 1 SeqLambdaD{ 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 "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "j")) ")" )) ")" ) ")" )) proof end; scheme :: FINSEQ_2:sch 2 IndSeqD{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool P1[(Set ($#k6_finseq_1 :::"<*>"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "p"))])) "holds" (Bool P1[(Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))]))) proof end; theorem :: FINSEQ_2:24 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D1")) "holds" (Bool (Set (Var "p")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:25 (Bool "for" (Set (Var "i")) "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_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set (Var "D")) "holds" (Bool (Set (Var "f")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "p")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "," (Set (Var "D"))))) ; theorem :: FINSEQ_2:27 (Bool "for" (Set (Var "i")) "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_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" )) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:28 (Bool "for" (Set (Var "i")) "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 "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))))))) ; theorem :: FINSEQ_2:29 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: FINSEQ_2:30 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "q"))) "is" ($#m1_hidden :::"FinSequence":::)))))) ; theorem :: FINSEQ_2:31 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9"))))))) ; theorem :: FINSEQ_2:32 (Bool "for" (Set (Var "A")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:33 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "D9")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))))))) ; theorem :: FINSEQ_2:34 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))) ; theorem :: FINSEQ_2:35 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x1")) ($#k9_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))))) ; theorem :: FINSEQ_2:36 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))))) ; theorem :: FINSEQ_2:37 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x3")) ")" ) ($#k11_finseq_1 :::"*>"::: ) )))))) ; theorem :: FINSEQ_2:38 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "j")) ")" ) "st" (Bool "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_hidden :::"FinSequence":::))))) ; theorem :: FINSEQ_2:39 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_hidden :::"FinSequence":::))))) ; theorem :: FINSEQ_2:40 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_hidden :::"FinSequence":::)))) ; theorem :: FINSEQ_2:41 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))))) ; theorem :: FINSEQ_2:42 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: FINSEQ_2:43 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))))) ; theorem :: FINSEQ_2:44 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))))) ; theorem :: FINSEQ_2:45 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "j")) ")" ) "st" (Bool "(" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))))))) ; theorem :: FINSEQ_2:46 (Bool "for" (Set (Var "i")) "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 "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))))))) ; theorem :: FINSEQ_2:47 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:48 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" )) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; definitionlet "i" be ($#m1_hidden :::"Nat":::); func :::"idseq"::: "i" -> ($#m1_hidden :::"FinSequence":::) equals :: FINSEQ_2:def 1 (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "i" ")" )); end; :: deftheorem defines :::"idseq"::: FINSEQ_2:def 1 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" )))); registrationlet "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_finseq_2 :::"idseq"::: ) "k") -> "k" ($#v3_card_1 :::"-element"::: ) ; end; registration cluster (Set ($#k1_finseq_2 :::"idseq"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: FINSEQ_2:49 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))) "holds" (Bool (Set (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))))) ; theorem :: FINSEQ_2:50 (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ; theorem :: FINSEQ_2:51 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "i")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: FINSEQ_2:52 (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) )) ; theorem :: FINSEQ_2:53 (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) "," (Num 3) ($#k11_finseq_1 :::"*>"::: ) )) ; theorem :: FINSEQ_2:54 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: FINSEQ_2:55 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "k"))) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ))) ; theorem :: FINSEQ_2:56 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))) "is" ($#m1_hidden :::"FinSequence":::)))) ; registrationlet "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "k" ")" ) ($#k2_funcop_1 :::"-->"::: ) "a") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_hidden :::"set"::: ) ; func "i" :::"|->"::: "a" -> ($#m1_hidden :::"FinSequence":::) equals :: FINSEQ_2:def 2 (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "i" ")" ) ($#k7_funcop_1 :::"-->"::: ) "a"); end; :: deftheorem defines :::"|->"::: FINSEQ_2:def 2 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a")))))); registrationlet "k" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_hidden :::"set"::: ) ; cluster (Set "k" ($#k2_finseq_2 :::"|->"::: ) "a") -> "k" ($#v3_card_1 :::"-element"::: ) ; end; theorem :: FINSEQ_2:57 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "d")) "," (Set (Var "w")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ; theorem :: FINSEQ_2:58 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FINSEQ_2:59 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 1) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: FINSEQ_2:60 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: FINSEQ_2:61 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 2) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: FINSEQ_2:62 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 3) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a")) ($#k11_finseq_1 :::"*>"::: ) ))) ; theorem :: FINSEQ_2:63 (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 "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "k")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "d"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))))) ; theorem :: FINSEQ_2:64 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#m1_hidden :::"FinSequence":::)))) ; theorem :: FINSEQ_2:65 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "q")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" )))) ; theorem :: FINSEQ_2:66 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) "is" ($#m1_hidden :::"FinSequence":::))))) ; theorem :: FINSEQ_2:67 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))))) ; theorem :: FINSEQ_2:68 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) "is" ($#m1_hidden :::"FinSequence":::))))) ; theorem :: FINSEQ_2:69 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))))) ; theorem :: FINSEQ_2:70 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "E"))))))) ; theorem :: FINSEQ_2:71 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ")" ))))))) ; theorem :: FINSEQ_2:72 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) ")" )))))) ; theorem :: FINSEQ_2:73 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p9")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) "," (Set (Var "p9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "E")))) & (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D9")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "E")))) ")" ))))) ; theorem :: FINSEQ_2:74 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d1")) ($#k12_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d19")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d19")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQ_2:75 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "," (Set (Var "d29")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d19")) "," (Set (Var "d29")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d19")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d29")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQ_2:76 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "," (Set (Var "d29")) "," (Set (Var "d39")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d19")) "," (Set (Var "d29")) "," (Set (Var "d39")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d19")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d29")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d39")) ")" ")" ) ($#k11_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQ_2:77 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "E"))))))) ; theorem :: FINSEQ_2:78 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))))))) ; theorem :: FINSEQ_2:79 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D9")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "E"))))))) ; theorem :: FINSEQ_2:80 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d19")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d19")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:81 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "," (Set (Var "d29")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d19")) "," (Set (Var "d29")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d19")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d29")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:82 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d19")) "," (Set (Var "d29")) "," (Set (Var "d39")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d19")) "," (Set (Var "d29")) "," (Set (Var "d39")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d19")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d29")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d39")) ")" ")" ) ($#k11_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:83 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "E"))))))) ; theorem :: FINSEQ_2:84 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))))))) ; theorem :: FINSEQ_2:85 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "E"))))))) ; theorem :: FINSEQ_2:86 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d1")) ($#k12_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d9")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:87 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d9")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d9")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQ_2:88 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d9")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d9")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d9")) ")" ")" ) ($#k11_finseq_1 :::"*>"::: ) ))))))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; mode :::"FinSequenceSet"::: "of" "D" -> ($#m1_hidden :::"set"::: ) means :: FINSEQ_2:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D")); end; :: deftheorem defines :::"FinSequenceSet"::: FINSEQ_2:def 3 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "D"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "a")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")))) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Const "D")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "S" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" "D"; end; theorem :: FINSEQ_2:89 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k13_finseq_1 :::"*"::: ) ) "is" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "D")))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; :: original: :::"*"::: redefine func "D" :::"*"::: -> ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" "D"; end; theorem :: FINSEQ_2:90 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D9")) "being" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "D9")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) )))) ; theorem :: FINSEQ_2:91 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "S")) "being" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "D9")) "holds" (Bool (Set (Var "S")) "is" ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Var "D")))))) ; registrationlet "i" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() "i" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_card_3 :::"countable"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "D"; end; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode Tuple of "i" "," "D" is "i" ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "D" be ($#m1_hidden :::"set"::: ) ; func "i" :::"-tuples_on"::: "D" -> ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" "D" equals :: FINSEQ_2:def 4 "{" (Set (Var "s")) where s "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "i") "}" ; end; :: deftheorem defines :::"-tuples_on"::: FINSEQ_2:def 4 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) "}" ))); registrationlet "i" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "i" be ($#m1_hidden :::"Nat":::); cluster -> "i" ($#v3_card_1 :::"-element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; theorem :: FINSEQ_2:92 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "z")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "z")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; theorem :: FINSEQ_2:93 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set (Var "D")) ")" )))) ; theorem :: FINSEQ_2:94 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "D")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: FINSEQ_2:95 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ))))) ; theorem :: FINSEQ_2:96 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) where d "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) : (Bool verum) "}" )) ; theorem :: FINSEQ_2:97 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Num 1) "," (Set (Var "D")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: FINSEQ_2:98 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; theorem :: FINSEQ_2:99 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ) where d1, d2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) : (Bool verum) "}" )) ; theorem :: FINSEQ_2:100 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Num 2) "," (Set (Var "D")) (Bool "ex" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ))))) ; theorem :: FINSEQ_2:101 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; theorem :: FINSEQ_2:102 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) ) where d1, d2, d3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) : (Bool verum) "}" )) ; theorem :: FINSEQ_2:103 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Num 3) "," (Set (Var "D")) (Bool "ex" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) ))))) ; theorem :: FINSEQ_2:104 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))) ; theorem :: FINSEQ_2:105 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "z")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t")) ")" ) where z "is" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")), t "is" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "j")) "," (Set (Var "D")) : (Bool verum) "}" ))) ; theorem :: FINSEQ_2:106 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 "s")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) "," (Set (Var "D")) (Bool "ex" (Set (Var "z")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))(Bool "ex" (Set (Var "t")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "j")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t"))))))))) ; theorem :: FINSEQ_2:107 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "j")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "z")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t"))) "is" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) "," (Set (Var "D"))))))) ; theorem :: FINSEQ_2:108 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ))) ; theorem :: FINSEQ_2:109 (Bool "for" (Set (Var "i")) "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 "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Var "z")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))))) ; theorem :: FINSEQ_2:110 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))))) ; theorem :: FINSEQ_2:111 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "i"))) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) ; theorem :: FINSEQ_2:112 (Bool "for" (Set (Var "i")) "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 "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "d"))) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))))))) ; theorem :: FINSEQ_2:113 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "z"))) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D9")))))))) ; theorem :: FINSEQ_2:114 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "z")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))))))) ; theorem :: FINSEQ_2:115 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "holds" (Bool (Set (Set (Var "z")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D"))))))) ; theorem :: FINSEQ_2:116 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: FINSEQ_2:117 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "D")) (Bool "ex" (Set (Var "t")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQ_2:118 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "z")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z")))))) ; theorem :: FINSEQ_2:119 (Bool "for" (Set (Var "i")) "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 "z1")) "," (Set (Var "z2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "z1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))))) ; theorem :: FINSEQ_2:120 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "z1")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "z2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "E"))))))))) ; theorem :: FINSEQ_2:121 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "z")) ")" ) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "E"))))))))) ; theorem :: FINSEQ_2:122 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "z")) "," (Set (Var "d9")) ")" ) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "E"))))))))) ; theorem :: FINSEQ_2:123 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "j")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x")) ")" ))))) ; theorem :: FINSEQ_2:124 (Bool "for" (Set (Var "i")) "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 "x")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))))) ; theorem :: FINSEQ_2:125 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ; theorem :: FINSEQ_2:126 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z")) ")" ) ($#k11_finseq_1 :::"*>"::: ) )))) ; theorem :: FINSEQ_2:127 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FINSEQ_2:128 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))) ; begin theorem :: FINSEQ_2:129 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r1_tarski :::"c="::: ) (Set (Var "q"))) & (Bool (Set (Var "p2")) ($#r1_tarski :::"c="::: ) (Set (Var "q"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2")))) ; theorem :: FINSEQ_2:130 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))(Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "w")))))))) ; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"|->"::: redefine func "n" :::"|->"::: "d" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; theorem :: FINSEQ_2:131 (Bool "for" (Set (Var "i")) "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 "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D"))) "iff" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")))) ")" )))) ; theorem :: FINSEQ_2:132 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" )))) ; theorem :: FINSEQ_2:133 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" )))) ; theorem :: FINSEQ_2:134 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) )))) ; theorem :: FINSEQ_2:135 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) )) ")" )) ")" )) ; theorem :: FINSEQ_2:136 (Bool "for" (Set (Var "A")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ; theorem :: FINSEQ_2:137 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) )) ")" )) ")" )) ; theorem :: FINSEQ_2:138 (Bool "for" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ; theorem :: FINSEQ_2:139 (Bool "for" (Set (Var "A")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) )) ")" )) ")" )) ; theorem :: FINSEQ_2:140 (Bool "for" (Set (Var "A")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ; theorem :: FINSEQ_2:141 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "x")) "is" (Set (Var "b1")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::)))) ; theorem :: FINSEQ_2:142 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) )))) ; theorem :: FINSEQ_2:143 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "m"))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func "M" :::"#"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "I" ($#k3_finseq_2 :::"*"::: ) ) means :: FINSEQ_2:def 5 (Bool "for" (Set (Var "i")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "I" ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" "M" ($#k3_relat_1 :::"*"::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"#"::: FINSEQ_2:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Set (Var "I")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k6_finseq_2 :::"#"::: ) )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "I")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "M")) ($#k3_relat_1 :::"*"::: ) (Set (Var "i")) ")" )))) ")" )))); registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster (Set "M" ($#k6_finseq_2 :::"#"::: ) ) -> bbbadV2_RELAT_1() ; end; definitionlet "a" be ($#m1_hidden :::"set"::: ) ; func :::"*-->"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) means :: FINSEQ_2:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) "a"))); end; :: deftheorem defines :::"*-->"::: FINSEQ_2:def 6 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a"))))) ")" ))); theorem :: FINSEQ_2:144 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "b")))))) ; theorem :: FINSEQ_2:145 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "M")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_finseq_2 :::"*-->"::: ) (Set (Var "a")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set (Var "D")) ")" )))))) ; theorem :: FINSEQ_2:146 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))) ; registrationlet "i" be ($#m1_hidden :::"Nat":::); cluster (Set "i" ($#k2_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#v3_relat_1 :::"empty-yielding"::: ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) for ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" "D"; end;