:: VECTSP_9  semantic presentation begin  



















registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))); 
end; 
theorem :: VECTSP_9:1 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (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 "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")) ")" )  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P"))))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "G")) ")" )))))))) ; 
 
theorem :: VECTSP_9:2 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))))))) ; 
 
theorem :: VECTSP_9:3 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))))))) ; 
 
theorem :: VECTSP_9:4 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) (Bool  "ex" (Set (Var "K")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")) ")" ))) & (Bool (Set (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "K"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F"))))  ")" )))))) ; 
 
theorem :: VECTSP_9:5 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")) ")" )))) "holds"  (Bool  "ex" (Set (Var "K")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A")) "st" (Bool (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "K")))))))))) ; 
 
theorem :: VECTSP_9:6 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")) ")" )))) "holds"  (Bool  "ex" (Set (Var "K")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A")) "st" (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "K"))))))))) ; 
 
theorem :: VECTSP_9:7 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool  "for" (Set (Var "K")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W")))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "K")))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "K"))))  ")" )))))) ; 
 
theorem :: VECTSP_9:8 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "K")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L"))))  ")" )))))) ; 
 
theorem :: VECTSP_9:9 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool  "ex" (Set (Var "K")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "W")) "st"  (Bool  "("  (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L"))))  ")" )))))) ; 
 
theorem :: VECTSP_9:10 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V"))  (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_vectsp_7 :::"Lin"::: )  (Set (Var "I")))))))) ; 
 registrationlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); 
cluster   ($#v1_vectsp_7 :::"linearly-independent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V"))); 
end; 
theorem :: VECTSP_9:11 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))))))) ; 
 
theorem :: VECTSP_9:12 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  ) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W"))))))) ; 
 
theorem :: VECTSP_9:13 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "B")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))))))) ; 
 
theorem :: VECTSP_9:14 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) "holds"  (Bool  "not" (Bool (Set (Var "v"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "B")))))))))) ; 
 
theorem :: VECTSP_9:15 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "I")))) "holds"  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "I"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "B")) "is"   ($#v1_vectsp_7 :::"linearly-dependent"::: )  )))))) ; 
 
theorem :: VECTSP_9:16 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A"))) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "W"))))))) ; 
 
theorem :: VECTSP_9:17 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "B"))))))))) ; 
 begin  
theorem :: VECTSP_9:18 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "v"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))) & (Bool (Bool  "not" (Set (Var "v"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "B")))))) "holds"  (Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "w"))  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )))  ")" )))))) ; 
 
theorem :: VECTSP_9:19 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#g1_vectsp_1 :::"VectSpStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"U5"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "V"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")))) & (Bool (Set (Var "B")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))) & (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "B")) ")" ))) & (Bool (Set   ($#g1_vectsp_1 :::"VectSpStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"U5"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "V"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  "(" (Set (Var "B"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "C")) ")" )))  ")" ))  ")" )))) ; 
 begin  
theorem :: VECTSP_9:20 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )) "holds"  (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Var "I")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: VECTSP_9:21 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: VECTSP_9:22 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "B"))))))) ; 
 
theorem :: VECTSP_9:23 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"  (Bool (Set   ($#k1_vectsp_4 :::"(0)."::: )  (Set (Var "V"))) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  ))) ; 
 
theorem :: VECTSP_9:24 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )) "holds"  (Bool (Set (Var "W")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )))) ; 
 registrationlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV13_ALGSTR_0()   ($#v7_vectsp_1 :::"strict"::: )   bbbadV8_VECTSP_1("GF") bbbadV9_VECTSP_1("GF") bbbadV10_VECTSP_1("GF") bbbadV11_VECTSP_1("GF") bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1()   ($#v1_matrlin :::"finite-dimensional"::: )    for    ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V"; 
end; registrationlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); 
cluster   ->   ($#v1_matrlin :::"finite-dimensional"::: )    for    ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V"; 
end; registrationlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV13_ALGSTR_0()   ($#v7_vectsp_1 :::"strict"::: )   bbbadV8_VECTSP_1("GF") bbbadV9_VECTSP_1("GF") bbbadV10_VECTSP_1("GF") bbbadV11_VECTSP_1("GF") bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1()   ($#v1_matrlin :::"finite-dimensional"::: )    for    ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V"; 
end; begin  definitionlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); assume 
(Bool (Set (Const "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )
 ; func  :::"dim"::: "V" ->   ($#m1_hidden :::"Nat":::) means :: VECTSP_9:def 1 (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" "V" "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "I"))))); end; 







:: deftheorem    defines :::"dim"::: VECTSP_9:def 1 :  (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v1_matrlin :::"finite-dimensional"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "I")) "being"    ($#m1_vectsp_7 :::"Basis"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "I")))))  ")" )))); 
 












theorem :: VECTSP_9:25 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V"))))))) ; 
 
theorem :: VECTSP_9:26 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: VECTSP_9:27 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "("  ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "V")) ")" ))))) ; 
 
theorem :: VECTSP_9:28 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W")))) "iff" (Bool (Set   ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "W"))))  ")" )))) ; 
 
theorem :: VECTSP_9:29 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"   (Bool  "("  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set   ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_4 :::"(0)."::: )  (Set (Var "V"))))  ")" ))) ; 
 
theorem :: VECTSP_9:30 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"   (Bool  "("  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Num 1)) "iff" (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))) & (Bool (Set   ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))  ")" ))  ")" ))) ; 
 
theorem :: VECTSP_9:31 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"   (Bool  "("  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Num 2)) "iff" (Bool  "ex" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "u"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is"   ($#v1_vectsp_7 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k2_vectsp_4 :::"(Omega)."::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) )))  ")" ))  ")" ))) ; 
 
theorem :: VECTSP_9:32 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "(" (Set (Var "W1"))  ($#k1_vectsp_5 :::"+"::: )  (Set (Var "W2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set  "(" (Set (Var "W1"))  ($#k2_vectsp_5 :::"/\"::: )  (Set (Var "W2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W2")) ")" )))))) ; 
 
theorem :: VECTSP_9:33 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set  "(" (Set (Var "W1"))  ($#k2_vectsp_5 :::"/\"::: )  (Set (Var "W2")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")) ")" )))))) ; 
 
theorem :: VECTSP_9:34 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V"))  ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: )  (Set (Var "W1")) "," (Set (Var "W2")))) "holds"  (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W2")) ")" )))))) ; 
 
theorem :: VECTSP_9:35 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))) "iff" (Bool  "ex" (Set (Var "W")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "st" (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))  ")" )))) ; 
 definitionlet "GF" be   ($#l6_algstr_0 :::"Field":::); let "V" be   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "GF")); let "n" be   ($#m1_hidden :::"Nat":::); func "n" :::"Subspaces_of"::: "V" ->    ($#m1_hidden :::"set"::: )   means :: VECTSP_9:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "W")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V" "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  "n")  ")" ))  ")" )); end; 







:: deftheorem    defines :::"Subspaces_of"::: VECTSP_9:def 2 :  (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b4")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_vectsp_9 :::"Subspaces_of"::: )  (Set (Var "V")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool  "ex" (Set (Var "W")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" ))  ")" ))  ")" ))))); 
 
theorem :: VECTSP_9:36 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V"))))) "holds"  (Bool  "not" (Bool (Set (Set (Var "n"))  ($#k2_vectsp_9 :::"Subspaces_of"::: )  (Set (Var "V"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 
theorem :: VECTSP_9:37 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  "st" (Bool (Bool (Set   ($#k1_vectsp_9 :::"dim"::: )  (Set (Var "V")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_vectsp_9 :::"Subspaces_of"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 
theorem :: VECTSP_9:38 (Bool  "for" (Set (Var "GF")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v1_matrlin :::"finite-dimensional"::: )    ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF"))  (Bool  "for" (Set (Var "W")) "being"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_vectsp_9 :::"Subspaces_of"::: )  (Set (Var "W")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "n"))  ($#k2_vectsp_9 :::"Subspaces_of"::: )  (Set (Var "V")))))))) ;