let V be Z_Module; :: thesis: for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
( v is torsion iff w is torsion )
let W be Subspace of V; :: thesis: for v being Vector of V
for w being Vector of W st v = w holds
( v is torsion iff w is torsion )
let v be Vector of V; :: thesis: for w being Vector of W st v = w holds
( v is torsion iff w is torsion )
let w be Vector of W; :: thesis: ( v = w implies ( v is torsion iff w is torsion ) )
assume A1: v = w ; :: thesis: ( v is torsion iff w is torsion )

hereby :: thesis: ( w is torsion implies v is torsion )

assume v is torsion ; :: thesis: w is torsion
then consider i being Element of INT.Ring such that
B2: ( i <> 0 & i * v = 0. V ) ;
i * w = i * v by A1, ZMODUL01:29
.= 0. W by ZMODUL01:26, B2 ;
hence w is torsion by B2; :: thesis: verum

end;

assume w is torsion ; :: thesis: v is torsion
then consider i being Element of INT.Ring such that
B2: ( i <> 0 & i * w = 0. W ) ;
i * v = i * w by A1, ZMODUL01:29
.= 0. V by ZMODUL01:26, B2 ;
hence v is torsion by B2; :: thesis: verum