:: RLVECT_3  semantic presentation begin  
































































theorem :: RLVECT_3:1 (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   ($#k6_rlvect_2 :::"Sum"::: )  (Set  "(" (Set (Var "L1"))  ($#k7_rlvect_2 :::"+"::: )  (Set (Var "L2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L2")) ")" ))))) ; 
 
theorem :: RLVECT_3:2 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (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   ($#k6_rlvect_2 :::"Sum"::: )  (Set  "(" (Set (Var "a"))  ($#k8_rlvect_2 :::"*"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")) ")" )))))) ; 
 
theorem :: RLVECT_3:3 (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   ($#k6_rlvect_2 :::"Sum"::: )  (Set  "("  ($#k9_rlvect_2 :::"-"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L")) ")" ))))) ; 
 
theorem :: RLVECT_3:4 (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   ($#k6_rlvect_2 :::"Sum"::: )  (Set  "(" (Set (Var "L1"))  ($#k10_rlvect_2 :::"-"::: )  (Set (Var "L2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L1")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "L2")) ")" ))))) ; 
 definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "A" is  :::"linearly-independent":::  means :: RLVECT_3:def 1 (Bool  "for" (Set (Var "l")) "being"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" "A"  "st" (Bool (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "V"))) "holds"  (Bool (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))); end; 





:: deftheorem    defines :::"linearly-independent"::: RLVECT_3:def 1 :  (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 (Set (Var "A")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) "iff" (Bool  "for" (Set (Var "l")) "being"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k3_rlvect_2 :::"Carrier"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))  ")" ))); 
 notationlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); antonym  :::"linearly-dependent"::: "A" for  :::"linearly-independent"::: ; end; 
theorem :: RLVECT_3:5 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ))) ; 
 
theorem :: RLVECT_3:6 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "not" (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))))) ; 
 
theorem :: RLVECT_3:7 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k1_subset_1 :::"{}"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) ; 
 registrationlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster   ($#v1_rlvect_3 :::"linearly-independent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 
end; 
theorem :: RLVECT_3:8 (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  ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) "iff" (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" ))) ; 
 
theorem :: RLVECT_3:9 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  "holds" (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is"   ($#v1_rlvect_3 :::"linearly-dependent"::: )  )) ; 
 
theorem :: RLVECT_3:10 (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  ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set (Var "v2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" ))) ; 
 
theorem :: RLVECT_3:11 (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  ($#k7_domain_1 :::"{"::: ) (Set (Var "v")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "is"   ($#v1_rlvect_3 :::"linearly-dependent"::: )  ) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is"   ($#v1_rlvect_3 :::"linearly-dependent"::: )  )  ")" ))) ; 
 
theorem :: RLVECT_3:12 (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")) "holds"   (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"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "v2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  "holds" (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v2"))))  ")" )  ")" )  ")" ))) ; 
 
theorem :: RLVECT_3:13 (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")) "holds"   (Bool  "("  (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"::: )  )  ")" ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v2")) ")" ))  ($#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"::: )  ))  ")" ))  ")" ))) ; 
 definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func  :::"Lin"::: "A" ->   ($#v1_rlvect_1 :::"strict"::: )     ($#m1_rlsub_1 :::"Subspace"::: )   "of" "V" means :: RLVECT_3:def 2 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")) ")" ) where l "is"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" "A" : (Bool verum)  "}"  ); end; 






:: deftheorem    defines :::"Lin"::: RLVECT_3:def 2 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_rlvect_1 :::"strict"::: )     ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")) ")" ) where l "is"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "A")) : (Bool verum)  "}"  )  ")" )))); 
 
theorem :: RLVECT_3:14 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))) "iff" (Bool  "ex" (Set (Var "l")) "being"    ($#m2_rlvect_2 :::"Linear_Combination"::: )   "of" (Set (Var "A")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rlvect_2 :::"Sum"::: )  (Set (Var "l")))))  ")" )))) ; 
 
theorem :: RLVECT_3:15 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A"))))))) ; 
 



theorem :: RLVECT_3:16 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rlsub_1 :::"(0)."::: )  (Set (Var "V"))))) ; 
 
theorem :: RLVECT_3:17 (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  "("   "not" (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_rlsub_1 :::"(0)."::: )  (Set (Var "V")))) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) ))  ")" ))) ; 
 
theorem :: RLVECT_3:18 (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 "W")) "being"   ($#v1_rlvect_1 :::"strict"::: )     ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "W")))))) ; 
 
theorem :: RLVECT_3:19 (Bool  "for" (Set (Var "V")) "being"   ($#v1_rlvect_1 :::"strict"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))))) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V"))))) ; 
 
theorem :: RLVECT_3:20 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A"))) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")))))) ; 
 
theorem :: RLVECT_3:21 (Bool  "for" (Set (Var "V")) "being"   ($#v1_rlvect_1 :::"strict"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "V"))))) ; 
 
theorem :: RLVECT_3:22 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" )  ($#k1_rlsub_2 :::"+"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: RLVECT_3:23 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" )  ($#k2_rlsub_2 :::"/\"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: RLVECT_3:24 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"U5"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "V"))) "#)" ))  ")" )))) ; 
 
theorem :: RLVECT_3:25 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "B")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))  ")" )))) ; 
 definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); mode  :::"Basis":::  "of" "V" ->   ($#m1_subset_1 :::"Subset":::) "of" "V" means :: RLVECT_3:def 3 (Bool  "("  (Bool it "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" "V") "," (Set  "the"  ($#u1_algstr_0 :::"U5"::: )  "of" "V") "," (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" "V") "#)" ))  ")" ); end; 





:: deftheorem    defines :::"Basis"::: RLVECT_3:def 3 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_rlvect_3 :::"Basis"::: )   "of" (Set (Var "V"))) "iff" (Bool  "("  (Bool (Set (Var "b2")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_rlvect_1 :::"RLSStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"U5"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_rlvect_1 :::"Mult"::: )  "of" (Set (Var "V"))) "#)" ))  ")" )  ")" ))); 
 



theorem :: RLVECT_3:26 (Bool  "for" (Set (Var "V")) "being"   ($#v1_rlvect_1 :::"strict"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_rlvect_3 :::"linearly-independent"::: )  )) "holds"  (Bool  "ex" (Set (Var "I")) "being"    ($#m1_rlvect_3 :::"Basis"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "I")))))) ; 
 
theorem :: RLVECT_3:27 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool  "ex" (Set (Var "I")) "being"    ($#m1_rlvect_3 :::"Basis"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))))) ; 
 
theorem :: RLVECT_3:28 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "CF")) "being"    ($#m1_orders_1 :::"Choice_Function"::: )   "of" (Set (Var "M"))  "st" (Bool (Bool (Bool  "not" (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "CF")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))))) ; 
 
theorem :: RLVECT_3:29 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_rlsub_1 :::"(0)."::: )  (Set (Var "V")))) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" ))) ; 
 
theorem :: RLVECT_3:30 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (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 "W3")))) "holds"  (Bool (Set (Set (Var "W1"))  ($#k2_rlsub_2 :::"/\"::: )  (Set (Var "W2"))) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "W3"))))) ; 
 
theorem :: RLVECT_3:31 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "W1")) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "W2"))) & (Bool (Set (Var "W1")) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "W3")))) "holds"  (Bool (Set (Var "W1")) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Set (Var "W2"))  ($#k2_rlsub_2 :::"/\"::: )  (Set (Var "W3")))))) ; 
 
theorem :: RLVECT_3:32 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (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 "W3"))) & (Bool (Set (Var "W2")) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "W3")))) "holds"  (Bool (Set (Set (Var "W1"))  ($#k1_rlsub_2 :::"+"::: )  (Set (Var "W2"))) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Var "W3"))))) ; 
 
theorem :: RLVECT_3:33 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "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 (Var "W1")) "is"    ($#m1_rlsub_1 :::"Subspace"::: )   "of" (Set (Set (Var "W2"))  ($#k1_rlsub_2 :::"+"::: )  (Set (Var "W3")))))) ; 
 
theorem :: RLVECT_3:34 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (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 :::"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  "(" (Set (Var "F"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k5_rlvect_2 :::"(#)"::: )  (Set (Var "F")) ")" )  ($#k8_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "f"))  ($#k5_rlvect_2 :::"(#)"::: )  (Set (Var "G")) ")" )))))) ;