let V, W be RealLinearSpace; :: thesis: for L being LinearOperator of V,W ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
let L be LinearOperator of V,W; :: thesis: ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
A1: the carrier of (Im L) = rng L by IMX2, LCL1;
A2: the carrier of (Ker L) = L " {(0. W)} by KLXY1, LCL1;
defpred S₁[ object , object ] means ex v being VECTOR of V st
( $1 = v + (Ker L) & $2 = L . v );
A3: for x being Element of the carrier of (VectQuot (V,(Ker L))) ex y being Element of the carrier of (Im L) st S₁[x,y]

proof

let x be Element of the carrier of (VectQuot (V,(Ker L))); :: thesis: ex y being Element of the carrier of (Im L) st S₁[x,y]
consider v being Point of V such that
A4: x = v + (Ker L) by LMQ07;
reconsider y = L . v as Element of the carrier of (Im L) by A1, FUNCT_2:4;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A4; :: thesis: verum

end;

consider QL being Function of the carrier of (VectQuot (V,(Ker L))), the carrier of (Im L) such that
A5: for x being Element of (VectQuot (V,(Ker L))) holds S₁[x,QL . x] from FUNCT_2:sch 3(A3);
A6: for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v

proof

let z be Point of (VectQuot (V,(Ker L))); :: thesis: for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v
let v be VECTOR of V; :: thesis: ( z = v + (Ker L) implies QL . z = L . v )
assume A7: z = v + (Ker L) ; :: thesis: QL . z = L . v
consider w being VECTOR of V such that
A8: ( z = w + (Ker L) & QL . z = L . w ) by A5;
consider v1 being Point of V such that
A9: ( v1 in Ker L & w = v + v1 ) by A7, A8, RLSUB_1:54, RLSUB_1:63;
w - v = v1 + (v - v) by A9, RLVECT_1:28
.= v1 + (0. V) by RLVECT_1:15
.= v1 by RLVECT_1:4 ;
then A10: ( w - v in the carrier of V & L . (w - v) in {(0. W)} ) by A2, A9, FUNCT_2:38;
L . (w - v) = L . (w + ((- 1) * v)) by RLVECT_1:16
.= (L . w) + (L . ((- 1) * v)) by VECTSP_1:def 20
.= (L . w) + ((- 1) * (L . v)) by LOPBAN_1:def 5
.= (L . w) + (- (L . v)) by RLVECT_1:16 ;
then (L . w) - (L . v) = 0. W by A10, TARSKI:def 1;
then L . v = ((L . w) - (L . v)) + (L . v) by RLVECT_1:4
.= (L . w) - ((L . v) - (L . v)) by RLVECT_1:29
.= (L . w) - (0. W) by RLVECT_1:15
.= L . w by RLVECT_1:13 ;
hence QL . z = L . v by A8; :: thesis: verum

end;

A11: for x1, x2 being object st x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 implies x1 = x2 )
assume A12: ( x1 in the carrier of (VectQuot (V,(Ker L))) & x2 in the carrier of (VectQuot (V,(Ker L))) & QL . x1 = QL . x2 ) ; :: thesis: x1 = x2
reconsider z1 = x1, z2 = x2 as Point of (VectQuot (V,(Ker L))) by A12;
consider v1 being VECTOR of V such that
A13: ( z1 = v1 + (Ker L) & QL . x1 = L . v1 ) by A5;
consider v2 being VECTOR of V such that
A14: ( z2 = v2 + (Ker L) & QL . x2 = L . v2 ) by A5;
(L . v1) - (L . v2) = (L . v1) + ((- 1) * (L . v2)) by RLVECT_1:16
.= (L . v1) + (L . ((- 1) * v2)) by LOPBAN_1:def 5
.= L . (v1 + ((- 1) * v2)) by VECTSP_1:def 20
.= L . (v1 - v2) by RLVECT_1:16 ;
then L . (v1 - v2) = 0. W by A12, A13, A14, RLVECT_1:15;
then L . (v1 - v2) in {(0. W)} by TARSKI:def 1;
then A15: v1 - v2 in Ker L by A2, FUNCT_2:38;
(v1 - v2) + v2 = v1 - (v2 - v2) by RLVECT_1:29
.= v1 - (0. V) by RLVECT_1:15
.= v1 by RLVECT_1:13 ;
then v1 in v2 + (Ker L) by A15;
hence x1 = x2 by A13, A14, RLSUB_1:54; :: thesis: verum

end;

for v being object st v in the carrier of (Im L) holds
ex s being object st
( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )

proof

let v be object ; :: thesis: ( v in the carrier of (Im L) implies ex s being object st
( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) )
assume v in the carrier of (Im L) ; :: thesis: ex s being object st
( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )
then v in rng L by IMX2, LCL1;
then consider x being object such that
A16: ( x in the carrier of V & L . x = v ) by FUNCT_2:11;
reconsider x = x as Point of V by A16;
reconsider s = x + (Ker L) as Point of (VectQuot (V,(Ker L))) by LMQ07;
take s ; :: thesis: ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s )
thus ( s in the carrier of (VectQuot (V,(Ker L))) & v = QL . s ) by A6, A16; :: thesis: verum

end;

then A17: QL is onto by FUNCT_2:10;
A18: for v, w being Element of (VectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)

proof

let v, w be Element of (VectQuot (V,(Ker L))); :: thesis: QL . (v + w) = (QL . v) + (QL . w)
consider x being Point of V such that
A19: v = x + (Ker L) by LMQ07;
consider y being Point of V such that
A20: w = y + (Ker L) by LMQ07;
A21: v + w = (x + y) + (Ker L) by A19, A20, LMQ11;
A22: QL . v = L . x by A6, A19;
A23: QL . w = L . y by A6, A20;
thus QL . (v + w) = L . (x + y) by A6, A21
.= (L . x) + (L . y) by VECTSP_1:def 20
.= (QL . v) + (QL . w) by A22, A23, RLSUB_1:13 ; :: thesis: verum

end;

for v being VECTOR of (VectQuot (V,(Ker L)))
for r being Real holds QL . (r * v) = r * (QL . v)

proof

let v be VECTOR of (VectQuot (V,(Ker L))); :: thesis: for r being Real holds QL . (r * v) = r * (QL . v)
let r be Real; :: thesis: QL . (r * v) = r * (QL . v)
consider x being Point of V such that
A24: v = x + (Ker L) by LMQ07;
r * v = (r * x) + (Ker L) by A24, LMQ09;
hence QL . (r * v) = L . (r * x) by A6
.= r * (L . x) by LOPBAN_1:def 5
.= r * (QL . v) by A6, A24, RLSUB_1:14 ;
:: thesis: verum

end;

then ( QL is additive & QL is homogeneous ) by A18, LOPBAN_1:def 5;
then reconsider QL = QL as LinearOperator of (VectQuot (V,(Ker L))),(Im L) ;
take QL ; :: thesis: ( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
thus QL is isomorphism by A11, A17, FUNCT_2:19; :: thesis: for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v
thus for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v by A6; :: thesis: verum