let V be Z_Module; :: thesis: ( V is divisible iff (Omega). V is divisible )

hereby :: thesis: ( (Omega). V is divisible implies V is divisible )

assume A1: V is divisible ; :: thesis: (Omega). V is divisible
for vv being Vector of ((Omega). V) holds vv is divisible

proof

let vv be Vector of ((Omega). V); :: thesis: vv is divisible
reconsider v = vv as Vector of V ;
B1: v is divisible by A1;
for a being Element of INT.Ring st a <> 0 holds
ex uu being Vector of ((Omega). V) st a * uu = vv

proof

let a be Element of INT.Ring; :: thesis: ( a <> 0 implies ex uu being Vector of ((Omega). V) st a * uu = vv )
assume C1: a <> 0 ; :: thesis: ex uu being Vector of ((Omega). V) st a * uu = vv
consider u being Vector of V such that
C2: a * u = v by B1, C1;
reconsider uu = u as Vector of ((Omega). V) ;
take uu ; :: thesis: a * uu = vv
thus a * uu = vv by C2; :: thesis: verum

end;

hence vv is divisible ; :: thesis: verum

end;

hence (Omega). V is divisible ; :: thesis: verum

end;

assume A1: (Omega). V is divisible ; :: thesis: V is divisible
for v being Vector of V holds v is divisible

proof

let v be Vector of V; :: thesis: v is divisible
reconsider vv = v as Vector of ((Omega). V) ;
B1: vv is divisible by A1;
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of V st a * u = v

proof

let a be Element of INT.Ring; :: thesis: ( a <> 0 implies ex u being Vector of V st a * u = v )
assume C1: a <> 0 ; :: thesis: ex u being Vector of V st a * u = v
consider uu being Vector of ((Omega). V) such that
C2: a * uu = vv by B1, C1;
reconsider u = uu as Vector of V ;
take u ; :: thesis: a * u = v
thus a * u = v by C2; :: thesis: verum

end;

hence v is divisible ; :: thesis: verum

end;

hence V is divisible ; :: thesis: verum