for x being object st x in A holds
x in the carrier of (Lin A)

proof

let x be object ; :: thesis:
assume A1: x in A ; :: thesis:
x in Lin A by A1, MOD_3:5;
hence x in the carrier of (Lin A) ; :: thesis:

end;

then A c= the carrier of (Lin A) ;
then reconsider AA = A as finite Subset of (Lin A) ;
Lin AA = Lin A by ZMODUL03:20;
hence Lin A is finitely-generated ; :: thesis: