let R be Ring; :: thesis:
let V be LeftMod of R; :: thesis:
let W1 be Submodule of V; :: thesis:
let W2 be Submodule of W1; :: thesis:
let U1 be Submodule of V; :: thesis:
let U2 be Submodule of VectQuot (V,U1); :: thesis:
assume A1: ( U1 = W2 & U2 = VectQuot (W1,W2) ) ; :: thesis:
set Z1 = VectQuot ((VectQuot (V,U1)),U2);
set Z2 = VectQuot (V,W1);
YY: rng (ZQMorph (V,U1)) = the carrier of (VectQuot (V,U1)) by FUNCT_2:def 3;
defpred S₁[ object , object ] means ex v being Element of V st
( $1 = v + U1 & $2 = v + W1 );
A2: for z being Element of (VectQuot (V,U1)) ex y being Element of (VectQuot (V,W1)) st S₁[z,y]

let z be Element of (VectQuot (V,U1)); :: thesis:
consider v being Element of V such that
A17: z = (ZQMorph (V,U1)) . v by FUNCT_2:113, YY;
A19: (ZQMorph (V,U1)) . v = v + U1 by defMophVW;
set y = v + W1;
v + W1 is Coset of W1 by VECTSP_4:def 6;
then v + W1 in CosetSet (V,W1) ;
then reconsider y = v + W1 as Element of (VectQuot (V,W1)) by VECTSP10:def 6;
take y ; :: thesis:
thus S₁[z,y] by A17, A19; :: thesis:

end;

consider f being Function of (VectQuot (V,U1)),(VectQuot (V,W1)) such that
A3: for z being Element of (VectQuot (V,U1)) holds S₁[z,f . z] from FUNCT_2:sch 3(A2);
f is linear-transformation of (VectQuot (V,U1)),(VectQuot (V,W1))

for x, y being Element of (VectQuot (V,U1)) holds f . (x + y) = (f . x) + (f . y)

let x, y be Element of (VectQuot (V,U1)); :: thesis:
consider xx being Element of V such that
C1: ( x = xx + U1 & f . x = xx + W1 ) by A3;
consider yy being Element of V such that
C2: ( y = yy + U1 & f . y = yy + W1 ) by A3;
consider xy being Element of V such that
C3: ( x + y = xy + U1 & f . (x + y) = xy + W1 ) by A3;
reconsider xU = xx + U1, yU = yy + U1 as Element of CosetSet (V,U1) by C1, C2, VECTSP10:def 6;
reconsider fxU = xx + W1, fyU = yy + W1 as Element of CosetSet (V,W1) by C1, C2, VECTSP10:def 6;
xy + U1 = (addCoset (V,U1)) . (xU,yU) by C3, C1, C2, VECTSP10:def 6
.= (xx + yy) + U1 by VECTSP10:def 3 ;
then xx + yy in xy + U1 by ZMODUL01:58;
then consider w being Vector of V such that
D21: ( xx + yy = xy + w & w in U1 ) ;
w in W1 by A1, D21, ZMODUL01:24;
then D3: xx + yy in xy + W1 by D21;
xx + yy in (xx + yy) + W1 by ZMODUL01:58;
then C4: xy + W1 = (xx + yy) + W1 by D3, ZMODUL01:68;
thus (f . x) + (f . y) = (addCoset (V,W1)) . (fxU,fyU) by C1, C2, VECTSP10:def 6
.= f . (x + y) by C4, C3, VECTSP10:def 3 ; :: thesis:

end;

then B1: f is additive ;
for a being Element of R
for x being Element of (VectQuot (V,U1)) holds f . (a * x) = a * (f . x)

let a be Element of R; :: thesis:
let x be Element of (VectQuot (V,U1)); :: thesis:
consider xx being Element of V such that
C1: ( x = xx + U1 & f . x = xx + W1 ) by A3;
consider ax being Element of V such that
C3: ( a * x = ax + U1 & f . (a * x) = ax + W1 ) by A3;
reconsider xU = xx + U1 as Element of CosetSet (V,U1) by C1, VECTSP10:def 6;
reconsider fxU = xx + W1 as Element of CosetSet (V,W1) by C1, VECTSP10:def 6;
ax + U1 = (lmultCoset (V,U1)) . (a,xU) by C3, C1, VECTSP10:def 6
.= (a * xx) + U1 by VECTSP10:def 5 ;
then a * xx in ax + U1 by ZMODUL01:58;
then consider w being Vector of V such that
D21: ( a * xx = ax + w & w in U1 ) ;
w in W1 by A1, D21, ZMODUL01:24;
then D3: a * xx in ax + W1 by D21;
a * xx in (a * xx) + W1 by ZMODUL01:58;
then C4: ax + W1 = (a * xx) + W1 by D3, ZMODUL01:68;
thus a * (f . x) = (lmultCoset (V,W1)) . (a,fxU) by C1, VECTSP10:def 6
.= f . (a * x) by C4, C3, VECTSP10:def 5 ; :: thesis:

end;

end;

then reconsider f = f as linear-transformation of (VectQuot (V,U1)),(VectQuot (V,W1)) ;
A4: ker f = U2

for v being Element of (VectQuot (V,U1)) holds
( v in ker f iff v in U2 )

let v be Element of (VectQuot (V,U1)); :: thesis:

assume v in ker f ; :: thesis:
then C1: f . v = 0. (VectQuot (V,W1)) by RANKNULL:10;
consider vv being Element of V such that
C2: ( v = vv + U1 & f . v = vv + W1 ) by A3;
vv + W1 = zeroCoset (V,W1) by C1, C2, VECTSP10:def 6
.= the carrier of W1 ;
then vv in W1 by ZMODUL01:63;
then reconsider vv1 = vv as Vector of W1 ;
for x being object holds
( x in vv + U1 iff x in vv1 + W2 )

let x be object ; :: thesis:

assume x in vv + U1 ; :: thesis:
then consider w3 being Vector of V such that
X1: ( x = vv + w3 & w3 in U1 ) ;
w3 in W1 by A1, X1, ZMODUL01:24;
then reconsider ww3 = w3 as Vector of W1 ;
X2: vv + w3 = vv1 + ww3 by ZMODUL01:28;
thus x in vv1 + W2 by A1, X1, X2; :: thesis:

end;

assume x in vv1 + W2 ; :: thesis:
then consider w2 being Vector of W1 such that
X1: ( x = vv1 + w2 & w2 in W2 ) ;
w2 in V by A1, X1, ZMODUL01:24;
then reconsider ww2 = w2 as Vector of V ;
X2: vv + ww2 = vv1 + w2 by ZMODUL01:28;
thus x in vv + U1 by A1, X1, X2; :: thesis:

end;

end;

assume v in U2 ; :: thesis:
then v in CosetSet (W1,W2) by A1, VECTSP10:def 6;
then ex A being Coset of W2 st v = A ;
then consider vv1 being Vector of W1 such that
X1: v = vv1 + W2 by VECTSP_4:def 6;
consider vv being Element of V such that
C2: ( v = vv + U1 & f . v = vv + W1 ) by A3;
vv in vv1 + W2 by C2, X1, ZMODUL01:58;
then vv in W1 ;
then f . v = zeroCoset (V,W1) by C2, ZMODUL01:63
.= 0. (VectQuot (V,W1)) by VECTSP10:def 6 ;
hence v in ker f by RANKNULL:10; :: thesis:

end;

end;

for y being object st y in the carrier of (VectQuot (V,W1)) holds
f " {y} <> {}

let y be object ; :: thesis:
assume C2: y in the carrier of (VectQuot (V,W1)) ; :: thesis:
y in CosetSet (V,W1) by C2, VECTSP10:def 6;
then consider yy being Coset of W1 such that
C8: y = yy ;
consider z being Element of V such that
C3: y = z + W1 by C8, VECTSP_4:def 6;
z + U1 is Coset of U1 by VECTSP_4:def 6;
then z + U1 in CosetSet (V,U1) ;
then reconsider y1 = z + U1 as Vector of (VectQuot (V,U1)) by VECTSP10:def 6;
consider z1 being Element of V such that
C6: ( y1 = z1 + U1 & f . y1 = z1 + W1 ) by A3;
z1 in z1 + U1 by ZMODUL01:58;
then consider w being Vector of V such that
D21: ( z1 = z + w & w in U1 ) by C6;
w in W1 by A1, D21, ZMODUL01:24;
then D3: z1 in z + W1 by D21;
z1 in z1 + W1 by ZMODUL01:58;
then y = f . y1 by C3, C6, D3, ZMODUL01:68;
then f . y1 in {y} by TARSKI:def 1;
hence f " {y} <> {} by FUNCT_2:38; :: thesis:

end;

end;