let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
let V be LeftMod of R; :: thesis: for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
let W be Subspace of V; :: thesis: for Ws being strict Subspace of V st Ws = (Omega). W holds
lmultCoset (V,W) = lmultCoset (V,Ws)
let Ws be strict Subspace 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 R
for A being Element of CosetSet (V,W) holds (lmultCoset (V,W)) . (z,A) = (lmultCoset (V,Ws)) . (z,A)

let z be Element of R; :: 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, VECTSP10:def 5
.= (z * a) + Ws by LmStrict11a, AS
.= (lmultCoset (V,Ws)) . (z,A) by A21, VECTSP10:def 5 ; :: thesis: verum

end;

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