let R be Ring; :: thesis: for V, U being LeftMod of R
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 (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
let V, U be LeftMod of R; :: thesis: 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 (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
let V1 be Submodule of V; :: thesis: 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 (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
let U1 be Submodule of U; :: thesis: 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 (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
let f be linear-transformation of V,U; :: thesis: ( f is onto & the carrier of V1 = f " the carrier of U1 implies ex F being linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective )
assume AS: ( f is onto & the carrier of V1 = f " the carrier of U1 ) ; :: thesis: ex F being linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) st F is bijective
set g = ZQMorph (U,U1);
reconsider V1s = (Omega). V1 as strict Submodule of V by ZMODUL01:42;
P2: (ZQMorph (U,U1)) * f is onto by AS, FUNCT_2:27;
P5: VectQuot (V,V1) = VectQuot (V,V1s) by ThStrict1;
the carrier of (ker ((ZQMorph (U,U1)) * f)) = f " the carrier of (ker (ZQMorph (U,U1))) by LMFirst3
.= f " the carrier of ((Omega). U1) by LMFirst5
.= the carrier of V1s by AS ;
then P3: ker ((ZQMorph (U,U1)) * f) = V1s by ZMODUL01:45;
P4: im ((ZQMorph (U,U1)) * f) = (Omega). (VectQuot (U,U1)) by P2, LMFirst4
.= VectQuot (U,U1) ;
then reconsider F = Zdecom ((ZQMorph (U,U1)) * f) as linear-transformation of (VectQuot (V,V1)),(VectQuot (U,U1)) by P3, P5;
take F ; :: thesis: F is bijective
Zdecom ((ZQMorph (U,U1)) * f) is bijective by defdecom;
hence F is bijective by P4; :: thesis: verum