set V0 = the Z_Module;
reconsider nilfunc = [: the carrier of ((0). the Z_Module), the carrier of ((0). the Z_Module):] --> 0 as Function of [: the carrier of ((0). the Z_Module), the carrier of ((0). the Z_Module):], the carrier of F_Real by FUNCOP_1:45;
set X0 = GenLat (((0). the Z_Module),nilfunc);
take GenLat (((0). the Z_Module),nilfunc) ; :: thesis: ( GenLat (((0). the Z_Module),nilfunc) is vector-distributive & GenLat (((0). the Z_Module),nilfunc) is scalar-distributive & GenLat (((0). the Z_Module),nilfunc) is scalar-associative & GenLat (((0). the Z_Module),nilfunc) is scalar-unital & GenLat (((0). the Z_Module),nilfunc) is Abelian & GenLat (((0). the Z_Module),nilfunc) is add-associative & GenLat (((0). the Z_Module),nilfunc) is right_zeroed & GenLat (((0). the Z_Module),nilfunc) is right_complementable & GenLat (((0). the Z_Module),nilfunc) is strict )
thus ( GenLat (((0). the Z_Module),nilfunc) is vector-distributive & GenLat (((0). the Z_Module),nilfunc) is scalar-distributive & GenLat (((0). the Z_Module),nilfunc) is scalar-associative & GenLat (((0). the Z_Module),nilfunc) is scalar-unital & GenLat (((0). the Z_Module),nilfunc) is Abelian & GenLat (((0). the Z_Module),nilfunc) is add-associative & GenLat (((0). the Z_Module),nilfunc) is right_zeroed & GenLat (((0). the Z_Module),nilfunc) is right_complementable & GenLat (((0). the Z_Module),nilfunc) is strict ) by ZMtoZL1; :: thesis: verum