set KT = ker T;
XX: ( T is additive & T is homogeneous ) ;
YY: rng (ZQMorph (V,(ker T))) = the carrier of (VectQuot (V,(ker T))) by FUNCT_2:def 3;
defpred S₁[ object , object ] means ex v being Element of V st
( $1 = (ZQMorph (V,(ker T))) . v & $2 = T . v );
A11: for z being Element of (VectQuot (V,(ker T))) ex y being Element of (im T) st S₁[z,y]

proof

let z be Element of (VectQuot (V,(ker T))); :: thesis: ex y being Element of (im T) st S₁[z,y]
consider v being Element of V such that
A12: z = (ZQMorph (V,(ker T))) . v by FUNCT_2:113, YY;
set y = T . v;
dom T = [#] V by LmDOMRNG;
then T . v in T .: ([#] V) by FUNCT_1:def 6;
then T . v in [#] (im T) by RANKNULL:def 2;
then reconsider y = T . v as Element of (im T) ;
take y ; :: thesis: S₁[z,y]
thus S₁[z,y] by A12; :: thesis: verum

end;

consider f being Function of the carrier of (VectQuot (V,(ker T))), the carrier of (im T) such that
A15: for z being Element of (VectQuot (V,(ker T))) holds S₁[z,f . z] from FUNCT_2:sch 3(A11);
A16: for v being Element of V holds f . ((ZQMorph (V,(ker T))) . v) = T . v

proof

let v1 be Element of V; :: thesis: f . ((ZQMorph (V,(ker T))) . v1) = T . v1
set z = (ZQMorph (V,(ker T))) . v1;
reconsider z = (ZQMorph (V,(ker T))) . v1 as Element of (VectQuot (V,(ker T))) ;
consider v2 being Element of V such that
Q1: ( z = (ZQMorph (V,(ker T))) . v2 & f . z = T . v2 ) by A15;
(ZQMorph (V,(ker T))) . v1 = v1 + (ker T) by defMophVW;
then Q3: v1 + (ker T) = v2 + (ker T) by Q1, defMophVW;
Q4: v1 in v1 + (ker T) by VECTSP_4:44;
A23: v2 in v1 + (ker T) by Q3, VECTSP_4:44;
(T . v1) - (T . v2) = T . (v1 - v2) by ZMODUL05:18
.= 0. W by A23, Q4, VECTSP_4:63, RANKNULL:10 ;
hence f . ((ZQMorph (V,(ker T))) . v1) = T . v1 by Q1, RLVECT_1:21; :: thesis: verum

end;

for x, y being Vector of (VectQuot (V,(ker T))) holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Vector of (VectQuot (V,(ker T))); :: thesis: f . (x + y) = (f . x) + (f . y)
consider v being Element of V such that
A17: x = (ZQMorph (V,(ker T))) . v by FUNCT_2:113, YY;
consider w being Element of V such that
A18: y = (ZQMorph (V,(ker T))) . w by FUNCT_2:113, YY;
A19: (ZQMorph (V,(ker T))) . v = v + (ker T) by defMophVW;
A20: (ZQMorph (V,(ker T))) . w = w + (ker T) by defMophVW;
reconsider A = v + (ker T) as Element of CosetSet (V,(ker T)) by A19, VECTSP10:def 6;
reconsider B = w + (ker T) as Element of CosetSet (V,(ker T)) by A20, VECTSP10:def 6;
x + y = (addCoset (V,(ker T))) . (A,B) by A17, A18, A19, A20, VECTSP10:def 6
.= (v + w) + (ker T) by VECTSP10:def 3 ;
then A22: x + y = (ZQMorph (V,(ker T))) . (v + w) by defMophVW;
A23: T . v = f . x by A16, A17;
A24: T . w = f . y by A16, A18;
thus f . (x + y) = T . (v + w) by A16, A22
.= (T . v) + (T . w) by XX
.= (f . x) + (f . y) by A23, A24, VECTSP_4:13 ; :: thesis: verum

end;

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

proof

let a be Element of R; :: thesis: for x being Element of (VectQuot (V,(ker T))) holds f . (a * x) = a * (f . x)
let x be Element of (VectQuot (V,(ker T))); :: thesis: f . (a * x) = a * (f . x)
consider v being Element of V such that
A2: ( x = (ZQMorph (V,(ker T))) . v & f . x = T . v ) by A15;
(ZQMorph (V,(ker T))) . (a * v) = a * x by A2, MOD_2:def 2;
hence f . (a * x) = T . (a * v) by A16
.= a * (T . v) by XX
.= a * (f . x) by A2, VECTSP_4:14 ;
:: thesis: verum

end;

then A17: f is homogeneous ;
for y being object st y in the carrier of (im T) holds
ex x being object st
( x in the carrier of (VectQuot (V,(ker T))) & y = f . x )

proof

let y be object ; :: thesis: ( y in the carrier of (im T) implies ex x being object st
( x in the carrier of (VectQuot (V,(ker T))) & y = f . x ) )
assume LA0: y in the carrier of (im T) ; :: thesis: ex x being object st
( x in the carrier of (VectQuot (V,(ker T))) & y = f . x )
the carrier of (im T) c= the carrier of W by VECTSP_4:def 2;
then reconsider y0 = y as Element of W by LA0;
y0 in im T by LA0;
then consider v being Element of V such that
LA1: y0 = T . v by RANKNULL:13;
f . ((ZQMorph (V,(ker T))) . v) = y by A16, LA1;
hence ex x being object st
( x in the carrier of (VectQuot (V,(ker T))) & y = f . x ) ; :: thesis: verum

end;

then rng f = the carrier of (im T) by FUNCT_2:10;
then A18: f is onto by FUNCT_2:def 3;
for x1, x2 being object st x1 in the carrier of (VectQuot (V,(ker T))) & x2 in the carrier of (VectQuot (V,(ker T))) & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in the carrier of (VectQuot (V,(ker T))) & x2 in the carrier of (VectQuot (V,(ker T))) & f . x1 = f . x2 implies x1 = x2 )
assume A19: ( x1 in the carrier of (VectQuot (V,(ker T))) & x2 in the carrier of (VectQuot (V,(ker T))) & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider xx1 = x1 as Element of (VectQuot (V,(ker T))) by A19;
reconsider xx2 = x2 as Element of (VectQuot (V,(ker T))) by A19;
consider v1 being Element of V such that
A20: ( xx1 = (ZQMorph (V,(ker T))) . v1 & f . xx1 = T . v1 ) by A15;
consider v2 being Element of V such that
A21: ( xx2 = (ZQMorph (V,(ker T))) . v2 & f . xx2 = T . v2 ) by A15;
A23: v1 - v2 in ker T by A19, A20, A21, RANKNULL:17;
A24: (ZQMorph (V,(ker T))) . v1 = v1 + (ker T) by defMophVW;
A25: (ZQMorph (V,(ker T))) . v2 = v2 + (ker T) by defMophVW;
(v1 - v2) + v2 = v1 - (v2 - v2) by RLVECT_1:29
.= v1 - (0. V) by RLVECT_1:15
.= v1 ;
then v1 in v2 + (ker T) by A23;
hence x1 = x2 by A24, A25, A21, A20, VECTSP_4:55; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:19;
hence ex b₁ being linear-transformation of (VectQuot (V,(ker T))),(im T) st
( b₁ is bijective & ( for v being Element of V holds b₁ . ((ZQMorph (V,(ker T))) . v) = T . v ) ) by A18, A16, A17, A25; :: thesis: verum