theorem :: ZMODUL07:39

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