theorem :: ZMODUL07:40

for V being Z_Module
for W1 being Submodule of V
for W2 being Submodule of W1
for U1 being Submodule of V
for U2 being Submodule of Z_ModuleQuot (V,U1) st U1 = W2 & U2 = Z_ModuleQuot (W1,W2) holds
ex F being linear-transformation of (Z_ModuleQuot ((Z_ModuleQuot (V,U1)),U2)),(Z_ModuleQuot (V,W1)) st F is bijective