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

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