let GF be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being LeftMod of GF holds (0). V is free
let V be LeftMod of GF; :: 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, Th9;
then B9 is base by A2;
hence (0). V is free ; :: thesis: verum