set V0 = the free finite-rank Z_Module;
reconsider nilfunc = [: the carrier of ((0). the free finite-rank Z_Module), the carrier of ((0). the free finite-rank Z_Module):] --> 0 as Function of [: the carrier of ((0). the free finite-rank Z_Module), the carrier of ((0). the free finite-rank Z_Module):], the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat (((0). the free finite-rank Z_Module),nilfunc);
reconsider X0 = GenLat (((0). the free finite-rank Z_Module),nilfunc) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring ;
reconsider X0 = X0 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free LatticeStr over INT.Ring ;
take X0 ; :: thesis: X0 is finite-rank
thus X0 is finite-rank by ZMtoZL3; :: thesis: verum