set V0 = the free Z_Module;
reconsider nilfunc = [: the carrier of ((0). the free Z_Module), the carrier of ((0). the free Z_Module):] --> 0 as Function of [: the carrier of ((0). the free Z_Module), the carrier of ((0). the free Z_Module):], the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat (((0). the free Z_Module),nilfunc);
reconsider X0 = GenLat (((0). the free 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 ;
take X0 ; :: thesis: X0 is torsion-free
thus X0 is torsion-free ; :: thesis: verum