theorem :: ZMODUL07:40

for R being Ring
for V being LeftMod of R
for W1 being Submodule of V
for W2 being Submodule of W1
for U1 being Submodule of V
for U2 being Submodule of VectQuot (V,U1) st U1 = W2 & U2 = VectQuot (W1,W2) holds
ex F being linear-transformation of (VectQuot ((VectQuot (V,U1)),U2)),(VectQuot (V,W1)) st F is bijective