let R be non degenerated Ring; :: thesis: Free_LMod ({},R) is free
set V = TrivialLMod R;
B0: Free_LMod ({},R) = TrivialLMod R by ThTriv1;
reconsider W1 = TrivialLMod R as strict Subspace of TrivialLMod R by VECTSP_4:24;
reconsider W2 = (0). (TrivialLMod R) as strict Subspace of TrivialLMod R ;
the carrier of W2 = {(0. (TrivialLMod R))} by VECTSP_4:def 3
.= {0} ;
then W1 = W2 by VECTSP_4:29;
then {} the carrier of (TrivialLMod R) is base by VECTSP_7:9;
hence Free_LMod ({},R) is free by B0; :: thesis: verum