:: RLVECT_X semantic presentation begin theorem :: RLVECT_X:1 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R2"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k1_binom :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: RLVECT_X:2 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R2")))) & (Bool (Set (Var "R3")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "R1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "R2"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: RLVECT_X:3 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "R2")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "a")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "R1"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" )))))) ; begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "i" be ($#m1_hidden :::"Integer":::); let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "i" :::"*"::: "L" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" means :: RLVECT_X:def 1 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "i" ($#k11_binop_2 :::"*"::: ) (Set "(" "L" ($#k1_seq_1 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"*"::: RLVECT_X:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "L")) "," (Set (Var "b4")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_rlvect_x :::"*"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k1_seq_1 :::"."::: ) (Set (Var "v")) ")" )))) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func :::"Z_Lin"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RLVECT_X:def 2 "{" (Set "(" ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l")) ")" ) where l "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" "A" : (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) )) "}" ; end; :: deftheorem defines :::"Z_Lin"::: RLVECT_X:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l")) ")" ) where l "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) : (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) )) "}" ))); theorem :: RLVECT_X:4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "l"))) ($#r1_rlvect_2 :::"="::: ) (Set (Set (Var "i")) ($#k1_rlvect_x :::"*"::: ) (Set (Var "l"))))))))) ; theorem :: RLVECT_X:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l1"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l2"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "l1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "l2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))))) ; theorem :: RLVECT_X:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "l"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "i")) ($#k1_rlvect_x :::"*"::: ) (Set (Var "l")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) )))))) ; theorem :: RLVECT_X:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: RLVECT_X:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set (Var "A")) ")" ))))) ; theorem :: RLVECT_X:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))))))) ; theorem :: RLVECT_X:10 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "i")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))))))) ; theorem :: RLVECT_X:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))))) ; theorem :: RLVECT_X:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))))))) ; theorem :: RLVECT_X:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "B")))))) ; theorem :: RLVECT_X:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RLVECT_X:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RLVECT_X:16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))) ")" )))) ; theorem :: RLVECT_X:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: RLVECT_X:18 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" )))) ; theorem :: RLVECT_X:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w2")) ")" )))) ")" )))) ; theorem :: RLVECT_X:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ))))) ; theorem :: RLVECT_X:21 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w2")) ")" )))) ")" )))) ; theorem :: RLVECT_X:22 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k8_domain_1 :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v3")) ")" )))) ")" )))) ; theorem :: RLVECT_X:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "w1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "w2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "w3")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: RLVECT_X:24 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w3")) ")" )))) ")" )))) ; theorem :: RLVECT_X:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "g1")) "," (Set (Var "h1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V"))(Bool "ex" (Set (Var "a1")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "h1")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1")) ")" )))) "holds" (Bool (Set (Set (Var "h1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))) ")" )))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) "n" ($#v3_card_1 :::"-element"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "RS" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "RS")); func :::"Z_Lin"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "RS" equals :: RLVECT_X:def 3 "{" (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g")) ")" ) where g "is" (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" "RS" : (Bool "ex" (Set (Var "a")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))))) "}" ; end; :: deftheorem defines :::"Z_Lin"::: RLVECT_X:def 3 : (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) "holds" (Bool (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g")) ")" ) where g "is" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) : (Bool "ex" (Set (Var "a")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))))) "}" ))); theorem :: RLVECT_X:26 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "g")) "being" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#v3_card_1 :::"-element"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS"))(Bool "ex" (Set (Var "a")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))) ")" )))) ; theorem :: RLVECT_X:27 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))))))) ; theorem :: RLVECT_X:28 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "RS")) ")" )))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "RS")))))) ; theorem :: RLVECT_X:29 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "RS")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "v")) ")" )))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_X:30 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f"))))))) ; theorem :: RLVECT_X:31 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))))) ; theorem :: RLVECT_X:32 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) (Bool "for" (Set (Var "s")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))))))) ; theorem :: RLVECT_X:33 (Bool "for" (Set (Var "RS")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "RS")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_x :::"Z_Lin"::: ) (Set (Var "f")))))) ; theorem :: RLVECT_X:34 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set (Var "A")))))) ; theorem :: RLVECT_X:35 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g1")) "," (Set (Var "h1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a1")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "h1")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g1")) ")" )))) "holds" (Bool (Set (Set (Var "h1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))))))))) ; theorem :: RLVECT_X:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set "(" ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A")))))) ; theorem :: RLVECT_X:37 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rlvect_x :::"Z_Lin"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set (Var "B")))))) ;