set V = the Z_Module;
take (0). the Z_Module ; :: thesis: ( (0). the Z_Module is strict & (0). the Z_Module is finite-rank )
thus ( (0). the Z_Module is strict & (0). the Z_Module is finite-rank ) ; :: thesis: verum