:: RLVECT_2 semantic presentation begin definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "x")) ($#r1_struct_0 :::"in"::: ) (Set (Const "S"))) ; func :::"vector"::: "(" "S" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "S" equals :: RLVECT_2:def 1 "x"; end; :: deftheorem defines :::"vector"::: RLVECT_2:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_rlvect_2 :::"vector"::: ) "(" (Set (Var "S")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))); theorem :: RLVECT_2:1 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_rlvect_2 :::"vector"::: ) "(" (Set (Var "S")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: RLVECT_2:2 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ))))) ; theorem :: RLVECT_2:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" )))))) ; theorem :: RLVECT_2:4 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; theorem :: RLVECT_2:5 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ))))) ; theorem :: RLVECT_2:6 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))))))) ; theorem :: RLVECT_2:7 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume (Bool "(" (Bool (Set (Const "V")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Const "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Const "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) ")" ) ; func :::"Sum"::: "T" -> ($#m1_subset_1 :::"Element":::) "of" "V" means :: RLVECT_2:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "T") & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")))) ")" )); end; :: deftheorem defines :::"Sum"::: RLVECT_2:def 2 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Var "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "T")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))) & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")))) ")" )) ")" )))); theorem :: RLVECT_2:8 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:9 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: RLVECT_2:10 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))))) ; theorem :: RLVECT_2:11 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3")))) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k8_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v3")))))) ; theorem :: RLVECT_2:12 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "T")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "T")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "S")) ")" ))))) ; theorem :: RLVECT_2:13 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "T")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "S")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: RLVECT_2:14 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "T")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "S")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: RLVECT_2:15 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k7_subset_1 :::"\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "S")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "S")) ")" ))))) ; theorem :: RLVECT_2:16 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k7_subset_1 :::"\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set (Var "T")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: RLVECT_2:17 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "S")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" ) ")" ))))) ; theorem :: RLVECT_2:18 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k5_subset_1 :::"\+\"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k7_subset_1 :::"\"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "S")) ($#k7_subset_1 :::"\"::: ) (Set (Var "T")) ")" ) ")" ))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; mode :::"Linear_Combination"::: "of" "V" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) means :: RLVECT_2:def 3 (Bool "ex" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))); end; :: deftheorem defines :::"Linear_Combination"::: RLVECT_2:def 3 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V"))) "iff" (Bool "ex" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ")" ))); notationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "L" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); synonym :::"Carrier"::: "L" for :::"support"::: "V"; end; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "L" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"Carrier"::: redefine func :::"Carrier"::: "L" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RLVECT_2:def 4 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool (Set "L" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ; end; :: deftheorem defines :::"Carrier"::: RLVECT_2:def 4 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ))); registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); cluster (Set ($#k13_pre_poly :::"Carrier"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: RLVECT_2:19 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))))) ")" )))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"ZeroLC"::: "V" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" means :: RLVECT_2:def 5 (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"ZeroLC"::: RLVECT_2:def 5 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")))) "iff" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); theorem :: RLVECT_2:20 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); mode :::"Linear_Combination"::: "of" "A" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" means :: RLVECT_2:def 6 (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) it) ($#r1_tarski :::"c="::: ) "A"); end; :: deftheorem defines :::"Linear_Combination"::: RLVECT_2:def 6 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )))); theorem :: RLVECT_2:21 (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")) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "l")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "B")))))) ; theorem :: RLVECT_2:22 (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_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V"))) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A"))))) ; theorem :: RLVECT_2:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set (Var "l")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "F" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "f" :::"(#)"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") means :: RLVECT_2:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (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 ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: RLVECT_2:def 7 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: RLVECT_2:24 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))))) ; theorem :: RLVECT_2:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))))))) ; theorem :: RLVECT_2:26 (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "v")) ($#k3_pre_poly :::"*>"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_pre_poly :::"*>"::: ) ))))) ; theorem :: RLVECT_2:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v2")) ")" ) ($#k2_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_2:28 (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")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k5_rlvect_2 :::"(#)"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v2")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v3")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v3")) ")" ) ($#k3_finseq_4 :::"*>"::: ) ))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func :::"Sum"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "V" means :: RLVECT_2:def 8 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) "L")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" "L" ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ))) ")" )); end; :: deftheorem defines :::"Sum"::: RLVECT_2:def 8 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "L")) ($#k5_rlvect_2 :::"(#)"::: ) (Set (Var "F")) ")" ))) ")" )) ")" )))); theorem :: RLVECT_2:29 (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 "(" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v1_rlsub_1 :::"linearly-closed"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))) ; theorem :: RLVECT_2:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:31 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_2:32 (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 "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_2:33 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v2")) ")" )))))) ; theorem :: RLVECT_2:34 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_2:35 (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 "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_2:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v2")) ")" )))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "L1", "L2" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); :: original: :::"="::: redefine pred "L1" :::"="::: "L2" means :: RLVECT_2:def 9 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "holds" (Bool (Set "L1" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "L2" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"="::: RLVECT_2:def 9 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r1_rlvect_2 :::"="::: ) (Set (Var "L2"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) ")" ))); definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "L1", "L2" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); :: original: :::"+"::: redefine func "L1" :::"+"::: "L2" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" means :: RLVECT_2:def 10 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "L1" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "L2" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"+"::: RLVECT_2:def 10 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "b4")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ))); theorem :: RLVECT_2:37 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L2")) ")" ))))) ; theorem :: RLVECT_2:38 (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" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L1")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "L2")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2"))) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))))) ; theorem :: RLVECT_2:39 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2"))) ($#r1_rlvect_2 :::"="::: ) (Set (Set (Var "L2")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L1")))))) ; theorem :: RLVECT_2:40 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set (Var "L2")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L3")) ")" )) ($#r1_rlvect_2 :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L3")))))) ; theorem :: RLVECT_2:41 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k7_rlvect_2 :::"+"::: ) (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" )) ($#r1_rlvect_2 :::"="::: ) (Set (Var "L"))) & (Bool (Set (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L"))) ($#r1_rlvect_2 :::"="::: ) (Set (Var "L"))) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "a" be ($#m1_subset_1 :::"Real":::); let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "a" :::"*"::: "L" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" means :: RLVECT_2:def 11 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k8_real_1 :::"*"::: ) (Set "(" "L" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"*"::: RLVECT_2:def 11 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" )))); theorem :: RLVECT_2:42 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))))))) ; theorem :: RLVECT_2:43 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))) ($#r1_rlvect_2 :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")))))) ; theorem :: RLVECT_2:44 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A"))))))) ; theorem :: RLVECT_2:45 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))) ($#r1_rlvect_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")) ")" )))))) ; theorem :: RLVECT_2:46 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set "(" (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2")) ")" )) ($#r1_rlvect_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" )))))) ; theorem :: RLVECT_2:47 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_rlvect_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))))))) ; theorem :: RLVECT_2:48 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Num 1) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))) ($#r1_rlvect_2 :::"="::: ) (Set (Var "L"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func :::"-"::: "L" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" equals :: RLVECT_2:def 12 (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_rlvect_2 :::"*"::: ) "L"); end; :: deftheorem defines :::"-"::: RLVECT_2:def 12 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L")))))); theorem :: RLVECT_2:49 (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 "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))))) ; theorem :: RLVECT_2:50 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2"))) ($#r1_rlvect_2 :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "L2")) ($#r1_rlvect_2 :::"="::: ) (Set ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L1")))))) ; theorem :: RLVECT_2:51 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L")))))) ; theorem :: RLVECT_2:52 (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" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L"))) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))))) ; theorem :: RLVECT_2:53 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k9_rlvect_2 :::"-"::: ) (Set "(" ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L")) ")" )) ($#r1_rlvect_2 :::"="::: ) (Set (Var "L"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "L1", "L2" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "L1" :::"-"::: "L2" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" equals :: RLVECT_2:def 13 (Set "L1" ($#k7_rlvect_2 :::"+"::: ) (Set "(" ($#k9_rlvect_2 :::"-"::: ) "L2" ")" )); end; :: deftheorem defines :::"-"::: RLVECT_2:def 13 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set "(" ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L2")) ")" ))))); theorem :: RLVECT_2:54 (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 "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "L1")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))))) ; theorem :: RLVECT_2:55 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set (Var "L1")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L2")) ")" ))))) ; theorem :: RLVECT_2:56 (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" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L1")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "L2")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "L1")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L2"))) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")))))) ; theorem :: RLVECT_2:57 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L"))) ($#r1_rlvect_2 :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"LinComb"::: "V" -> ($#m1_hidden :::"set"::: ) means :: RLVECT_2:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V") ")" )); end; :: deftheorem defines :::"LinComb"::: RLVECT_2:def 14 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V"))) ")" )) ")" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k11_rlvect_2 :::"LinComb"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Const "V"))); func :::"@"::: "e" -> ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V" equals :: RLVECT_2:def 15 "e"; end; :: deftheorem defines :::"@"::: RLVECT_2:def 15 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "L" be ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func :::"@"::: "L" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) "V") equals :: RLVECT_2:def 16 "L"; end; :: deftheorem defines :::"@"::: RLVECT_2:def 16 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k13_rlvect_2 :::"@"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "L"))))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"LCAdd"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) "V" ")" ) means :: RLVECT_2:def 17 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) "V") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e2")) ")" )))); end; :: deftheorem defines :::"LCAdd"::: RLVECT_2:def 17 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_rlvect_2 :::"LCAdd"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e2")) ")" )))) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"LCMult"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) "V" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) "V" ")" ) means :: RLVECT_2:def 18 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e")) ")" ))))); end; :: deftheorem defines :::"LCMult"::: RLVECT_2:def 18 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_rlvect_2 :::"LCMult"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "e")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set "(" ($#k12_rlvect_2 :::"@"::: ) (Set (Var "e")) ")" ))))) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"LC_RLSpace"::: "V" -> ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: RLVECT_2:def 19 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) "V" ")" ) "," (Set "(" ($#k13_rlvect_2 :::"@"::: ) (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) "V" ")" ) ")" ) "," (Set "(" ($#k14_rlvect_2 :::"LCAdd"::: ) "V" ")" ) "," (Set "(" ($#k15_rlvect_2 :::"LCMult"::: ) "V" ")" ) "#)" ); end; :: deftheorem defines :::"LC_RLSpace"::: RLVECT_2:def 19 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k13_rlvect_2 :::"@"::: ) (Set "(" ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ")" ) "," (Set "(" ($#k14_rlvect_2 :::"LCAdd"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k15_rlvect_2 :::"LCMult"::: ) (Set (Var "V")) ")" ) "#)" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k16_rlvect_2 :::"LC_RLSpace"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ; end; registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k16_rlvect_2 :::"LC_RLSpace"::: ) "V") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; theorem :: RLVECT_2:58 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_rlvect_2 :::"LinComb"::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:59 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_2 :::"ZeroLC"::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:60 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k14_rlvect_2 :::"LCAdd"::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:61 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k15_rlvect_2 :::"LCMult"::: ) (Set (Var "V"))))) ; theorem :: RLVECT_2:62 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L1")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k7_rlvect_2 :::"+"::: ) (Set (Var "L2")))))) ; theorem :: RLVECT_2:63 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L"))))))) ; theorem :: RLVECT_2:64 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_rlvect_2 :::"-"::: ) (Set (Var "L")))))) ; theorem :: RLVECT_2:65 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L1")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_rlvect_2 :::"vector"::: ) "(" (Set "(" ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V")) ")" ) "," (Set (Var "L2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k10_rlvect_2 :::"-"::: ) (Set (Var "L2")))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func :::"LC_RLSpace"::: "A" -> ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k16_rlvect_2 :::"LC_RLSpace"::: ) "V") means :: RLVECT_2:def 20 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "l")) where l "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" "A" : (Bool verum) "}" ); end; :: deftheorem defines :::"LC_RLSpace"::: RLVECT_2:def 20 : (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 "b3")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set ($#k16_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k17_rlvect_2 :::"LC_RLSpace"::: ) (Set (Var "A")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "l")) where l "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "A")) : (Bool verum) "}" ) ")" )))); theorem :: RLVECT_2:66 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ))))))) ; theorem :: RLVECT_2:67 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ))))))) ; theorem :: RLVECT_2:68 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "H")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" )))))) ; theorem :: RLVECT_2:69 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: RLVECT_2:70 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "u")) ")" ))))))) ; theorem :: RLVECT_2:71 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "w")) ")" ))))))) ;