:: MOD_3  semantic presentation begin  
theorem :: MOD_3:1 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v6_struct_0  "non"   ($#v6_struct_0 :::"degenerated"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l6_algstr_0 :::"doubleLoopStr"::: )    "holds" (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "R")) ")" )))) ; 
 



























theorem :: MOD_3:2 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_vectsp_6 :::"Carrier"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool  "ex" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_rlvect_1 :::"Sum"::: )  (Set  "(" (Set (Var "L"))  ($#k3_vectsp_6 :::"(#)"::: )  (Set (Var "F")) ")" )))  ")" )))))) ; 
 
theorem :: MOD_3:3 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set  "(" (Set (Var "a"))  ($#k6_vectsp_6 :::"*"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "L")) ")" ))))))) ; 
 


















definitionlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "V" be   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func  :::"Lin"::: "A" ->   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" "V" means :: MOD_3:def 1 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "l")) ")" ) where l "is"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" "A" : (Bool verum)  "}"  ); end; 







:: deftheorem    defines :::"Lin"::: MOD_3:def 1 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "l")) ")" ) where l "is"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A")) : (Bool verum)  "}"  )  ")" ))))); 
 
theorem :: MOD_3:4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_mod_3 :::"Lin"::: )  (Set (Var "A")))) "iff" (Bool  "ex" (Set (Var "l")) "being"    ($#m2_vectsp_6 :::"Linear_Combination"::: )   "of" (Set (Var "A")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_vectsp_6 :::"Sum"::: )  (Set (Var "l")))))  ")" ))))) ; 
 
theorem :: MOD_3:5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_mod_3 :::"Lin"::: )  (Set (Var "A")))))))) ; 
 
theorem :: MOD_3:6 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set  "("  ($#k1_subset_1 :::"{}"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_4 :::"(0)."::: )  (Set (Var "V")))))) ; 
 
theorem :: MOD_3:7 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "holds"  (Bool  "("   "not" (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_vectsp_4 :::"(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 :: MOD_3:8 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "W")) "being"   ($#v7_vectsp_1 :::"strict"::: )     ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "W"))))) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "W"))))))) ; 
 
theorem :: MOD_3:9 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#v7_vectsp_1 :::"strict"::: )    ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "R")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))))) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))))) ; 
 
theorem :: MOD_3:10 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_mod_3 :::"Lin"::: )  (Set (Var "A"))) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "B"))))))) ; 
 
theorem :: MOD_3:11 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))))) ; 
 
theorem :: MOD_3:12 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")) ")" )  ($#k1_vectsp_5 :::"+"::: )  (Set  "("  ($#k1_mod_3 :::"Lin"::: )  (Set (Var "B")) ")" )))))) ; 
 
theorem :: MOD_3:13 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )) "is"    ($#m1_vectsp_4 :::"Subspace"::: )   "of" (Set (Set  "("  ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")) ")" )  ($#k2_vectsp_5 :::"/\"::: )  (Set  "("  ($#k1_mod_3 :::"Lin"::: )  (Set (Var "B")) ")" )))))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "V" be   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); let "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "IT" is  :::"base":::  means :: MOD_3:def 2 (Bool  "("  (Bool "IT" "is"   ($#v1_lmod_5 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  "IT")  ($#r1_hidden :::"="::: )  (Set   ($#g1_vectsp_1 :::"VectSpStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V") "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "V") "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" "V") "," (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" "V") "#)" ))  ")" ); end; 






:: deftheorem    defines :::"base"::: MOD_3:def 2 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_mod_3 :::"base"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_lmod_5 :::"linearly-independent"::: )  ) & (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_vectsp_1 :::"VectSpStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u2_struct_0 :::"ZeroF"::: )  "of" (Set (Var "V"))) "," (Set  "the"  ($#u1_vectsp_1 :::"lmult"::: )  "of" (Set (Var "V"))) "#)" ))  ")" )  ")" )))); 
 definitionlet "R" be   ($#l6_algstr_0 :::"Ring":::); let "IT" be   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); attr "IT" is  :::"free":::  means :: MOD_3:def 3 (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "IT" "st" (Bool (Set (Var "B")) "is"   ($#v1_mod_3 :::"base"::: )  )); end; 





:: deftheorem    defines :::"free"::: MOD_3:def 3 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_mod_3 :::"free"::: )  ) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "B")) "is"   ($#v1_mod_3 :::"base"::: )  ))  ")" ))); 
 
theorem :: MOD_3:14 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Ring":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k1_vectsp_4 :::"(0)."::: )  (Set (Var "V"))) "is"   ($#v2_mod_3 :::"free"::: )  ))) ; 
 registrationlet "R" be   ($#l6_algstr_0 :::"Ring":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v7_vectsp_1 :::"strict"::: )     ($#v8_vectsp_1 :::"vector-distributive"::: )     ($#v9_vectsp_1 :::"scalar-distributive"::: )     ($#v10_vectsp_1 :::"scalar-associative"::: )     ($#v11_vectsp_1 :::"scalar-unital"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#v2_mod_3 :::"free"::: )    for    ($#l1_vectsp_1 :::"VectSpStr"::: )   "over" "R"; 
end; 



















theorem :: MOD_3:15 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_lmod_5 :::"linearly-independent"::: )  ) "iff" (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))  ")" )))) ; 
 
theorem :: MOD_3:16 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_lmod_5 :::"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 :::"Scalar":::) "of" (Set (Var "R"))  "holds" (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v2"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: MOD_3:17 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (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_lmod_5 :::"linearly-independent"::: )  )  ")" ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k4_vectsp_1 :::"*"::: )  (Set (Var "v2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))))  ")" ))  ")" )))) ; 
 
theorem :: MOD_3:18 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_lmod_5 :::"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_mod_3 :::"base"::: )  )  ")" ))))) ; 
 
theorem :: MOD_3:19 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_mod_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_mod_3 :::"base"::: )  )  ")" ))))) ; 
 
theorem :: MOD_3:20 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Var "V")) "is"   ($#v2_mod_3 :::"free"::: )  ))) ; 
 definitionlet "R" be   ($#l6_algstr_0 :::"Skew-Field":::); let "V" be   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); mode  :::"Basis":::  "of" "V" ->   ($#m1_subset_1 :::"Subset":::) "of" "V" means :: MOD_3:def 4 (Bool it "is"   ($#v1_mod_3 :::"base"::: )  ); end; 






:: deftheorem    defines :::"Basis"::: MOD_3:def 4 :  (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_mod_3 :::"Basis"::: )   "of" (Set (Var "V"))) "iff" (Bool (Set (Var "b3")) "is"   ($#v1_mod_3 :::"base"::: )  )  ")" )))); 
 
theorem :: MOD_3:21 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_lmod_5 :::"linearly-independent"::: )  )) "holds"  (Bool  "ex" (Set (Var "I")) "being"    ($#m1_mod_3 :::"Basis"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "I"))))))) ; 
 
theorem :: MOD_3:22 (Bool  "for" (Set (Var "R")) "being"   ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k1_mod_3 :::"Lin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool  "ex" (Set (Var "I")) "being"    ($#m1_mod_3 :::"Basis"::: )   "of" (Set (Var "V")) "st" (Bool (Set (Var "I"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))))) ;