:: RLVECT_4 semantic presentation begin scheme :: RLVECT_4:sch 1 LambdaSep3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F8() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F9( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F7 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F5 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F8 "(" ")" )) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set F3 "(" ")" )) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set F4 "(" ")" )) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set F5 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set F9 "(" (Set (Var "C")) ")" )) ")" ) ")" )) provided (Bool (Set F3 "(" ")" ) ($#r1_hidden :::"<>"::: ) (Set F4 "(" ")" )) and (Bool (Set F3 "(" ")" ) ($#r1_hidden :::"<>"::: ) (Set F5 "(" ")" )) and (Bool (Set F4 "(" ")" ) ($#r1_hidden :::"<>"::: ) (Set F5 "(" ")" )) proof end; theorem :: RLVECT_4:1 (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 (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set "(" (Set (Var "w")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set (Var "w")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "w"))) ")" ))) ; theorem :: RLVECT_4:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))) ; theorem :: RLVECT_4:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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 ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_4:4 (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 "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: RLVECT_4:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W"))))))) ; theorem :: RLVECT_4:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k8_domain_1 :::"}"::: ) ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "u")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: RLVECT_4:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))) ; theorem :: RLVECT_4:8 (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")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))) ")" )))) ; theorem :: RLVECT_4:9 (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")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: RLVECT_4:10 (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")) ($#k3_rlsub_1 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "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_4:11 (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")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"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_subset_1 :::"Real":::) "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_4:12 (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 "w1")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "w2")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: RLVECT_4:13 (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")) ($#k3_rlsub_1 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"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_subset_1 :::"Real":::) "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_4:14 (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")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"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_subset_1 :::"Real":::) "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_4:15 (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")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "w2")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "w3")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) ($#k8_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: RLVECT_4: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")) "," (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")) ($#k3_rlsub_1 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"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_subset_1 :::"Real":::) "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_4:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:19 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )))) ; theorem :: RLVECT_4:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )))) ; theorem :: RLVECT_4:22 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )))) ; theorem :: RLVECT_4:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "w")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:27 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )))) ; theorem :: RLVECT_4:28 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )))) ; theorem :: RLVECT_4:29 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ))) ; theorem :: RLVECT_4:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (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")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) "," (Set (Var "w")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )))) ; theorem :: RLVECT_4:32 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) "," (Set (Var "w")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )))) ; theorem :: RLVECT_4:33 (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")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: RLVECT_4:34 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) )))) "holds" (Bool "(" (Bool (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "w1")) "," (Set (Var "w2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set (Var "w1")) ($#r1_hidden :::"<>"::: ) (Set (Var "w2"))) ")" ))) ; theorem :: RLVECT_4:35 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "w")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "w")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w"))))))) ; theorem :: RLVECT_4:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k8_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-dependent"::: ) )) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: RLVECT_4:37 (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 :::"Real":::) (Bool "ex" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "st" (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; theorem :: RLVECT_4:38 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))))) ; theorem :: RLVECT_4:39 (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 "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3")))) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k8_domain_1 :::"}"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v3"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))))) ;