theorem :: ZMODUL07:38

for V, U being Z_Module
for V1 being Submodule of V
for U1 being Submodule of U
for f being linear-transformation of V,U st f is onto & the carrier of V1 = f " the carrier of U1 holds
ex F being linear-transformation of (Z_ModuleQuot (V,V1)),(Z_ModuleQuot (U,U1)) st F is bijective