set W = (0). V;
reconsider W = (0). V as Z_Module ;
set A = {} the carrier of W;
reconsider A = {} the carrier of W as Subset of W ;
Lin A = (0). W by ZMODUL02:67
.= (0). V by ZMODUL01:51 ;
hence (0). V is finitely-generated ; :: thesis: verum