let R be Ring; :: thesis: for V being LeftMod of R holds (0). V is free
let V be LeftMod of R; :: thesis: (0). V is free
set W = (0). V;
reconsider B9 = {} the carrier of V as Subset of ((0). V) by SUBSET_1:1;
reconsider V9 = V as Subspace of V by VECTSP_4:24;
A1: B9 = {} the carrier of ((0). V) ;
then A2: B9 is linearly-independent ;
(0). V9 = (0). ((0). V) by VECTSP_4:37;
then Lin B9 = (0). V by A1, Th6;
then B9 is base by A2;
hence (0). V is free ; :: thesis: verum