reconsider VV = (0). V as free Z_Module ;

ex A being finite Subset of VV st A is Basis of VV

ex A being finite Subset of VV st A is Basis of VV

proof

hence
(0). V is finite-rank
; :: thesis: verum
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;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