take (0). the Z_Module ; :: thesis: ( (0). the Z_Module is strict & (0). the Z_Module is free )
thus ( (0). the Z_Module is strict & (0). the Z_Module is free ) ; :: thesis: verum