let V be Z_Module; :: thesis: for W being Submodule of V
for Ws being strict Submodule of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
let W be Submodule of V; :: thesis: for Ws being strict Submodule of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
let Ws be strict Submodule of V; :: thesis: ( Ws = (Omega). W implies lmultCoset (V,W) = lmultCoset (V,Ws) )
assume AS: Ws = (Omega). W ; :: thesis: lmultCoset (V,W) = lmultCoset (V,Ws)
set f1 = lmultCoset (V,W);
set f2 = lmultCoset (V,Ws);
set C = CosetSet (V,W);
set Cs = CosetSet (V,Ws);
A14: CosetSet (V,W) = CosetSet (V,Ws) by AS, LmStrict1;

now :: thesis: for z being Element of INT.Ring
for A being Element of CosetSet (V,W) holds (lmultCoset (V,W)) . (z,A) = (lmultCoset (V,Ws)) . (z,A)

let z be Element of INT.Ring; :: thesis: for A being Element of CosetSet (V,W) holds (lmultCoset (V,W)) . (z,A) = (lmultCoset (V,Ws)) . (z,A)
let A be Element of CosetSet (V,W); :: thesis: (lmultCoset (V,W)) . (z,A) = (lmultCoset (V,Ws)) . (z,A)
A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A17: A1 = A ;
consider a being VECTOR of V such that
A18: A1 = a + W by VECTSP_4:def 6;
reconsider As = A as Element of CosetSet (V,Ws) by AS, LmStrict1;
A21: As = a + Ws by AS, A17, A18, LmStrict11a;
thus (lmultCoset (V,W)) . (z,A) = (z * a) + W by A17, A18, ZMODUL02:def 9
.= (z * a) + Ws by LmStrict11a, AS
.= (lmultCoset (V,Ws)) . (z,A) by A21, ZMODUL02:def 9 ; :: thesis: verum

end;

hence lmultCoset (V,W) = lmultCoset (V,Ws) by A14, BINOP_1:2; :: thesis: verum