set V = the free Z_Module;
take the free Z_Module ; :: thesis: ( the free Z_Module is torsion-free & the free Z_Module is free )
thus ( the free Z_Module is torsion-free & the free Z_Module is free ) ; :: thesis: verum