let R be non degenerated Ring; :: thesis: for X being set holds Free_LMod (X,R) is free
let X be set ; :: thesis: Free_LMod (X,R) is free

per cases ( X <> {} or X = {} ) ;

suppose X <> {} ; :: thesis: Free_LMod (X,R) is free

hence Free_LMod (X,R) is free by Th32; :: thesis: verum

end;

suppose X = {} ; :: thesis: Free_LMod (X,R) is free

hence Free_LMod (X,R) is free by Th33; :: thesis: verum

end;

end;