let V be Z_Module; :: thesis: for W being Submodule of V
for Ws being strict Submodule of V st Ws = (Omega). W holds
Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws)
let W be Submodule of V; :: thesis: for Ws being strict Submodule of V st Ws = (Omega). W holds
Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws)
let Ws be strict Submodule of V; :: thesis: ( Ws = (Omega). W implies Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws) )
assume A1: Ws = (Omega). W ; :: thesis: Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws)
set Z1 = Z_ModuleQuot (V,W);
set Z2 = Z_ModuleQuot (V,Ws);
A2: the carrier of (Z_ModuleQuot (V,W)) = CosetSet (V,W) by ZMODUL02:def 10
.= CosetSet (V,Ws) by A1, LmStrict1
.= the carrier of (Z_ModuleQuot (V,Ws)) by ZMODUL02:def 10 ;
A3: the addF of (Z_ModuleQuot (V,W)) = addCoset (V,W) by ZMODUL02:def 10
.= addCoset (V,Ws) by A1, LmStrict2
.= the addF of (Z_ModuleQuot (V,Ws)) by ZMODUL02:def 10 ;
A4: 0. (Z_ModuleQuot (V,W)) = zeroCoset (V,W) by ZMODUL02:def 10
.= zeroCoset (V,Ws) by A1
.= 0. (Z_ModuleQuot (V,Ws)) by ZMODUL02:def 10 ;
the lmult of (Z_ModuleQuot (V,W)) = lmultCoset (V,W) by ZMODUL02:def 10
.= lmultCoset (V,Ws) by A1, LmStrict3
.= the lmult of (Z_ModuleQuot (V,Ws)) by ZMODUL02:def 10 ;
hence Z_ModuleQuot (V,W) = Z_ModuleQuot (V,Ws) by A2, A3, A4; :: thesis: verum