reconsider VV = (0). V as free Z_Module ;
ex A being finite Subset of VV st A is Basis of VV
proof
set WW = {} the carrier of VV;
reconsider WW = {} the carrier of VV as Subset of VV ;
A1: Lin WW = (0). VV by ZMODUL02:67
.= VV by ZMODUL01:51 ;
reconsider WW = WW as finite Subset of VV ;
take WW ; :: thesis: WW is Basis of VV
thus WW is Basis of VV by A1, VECTSP_7:def 3; :: thesis: verum
end;
hence (0). V is finite-rank ; :: thesis: verum