let V be RealLinearSpace; :: thesis: for W being Subspace of V ex QL being LinearOperator of V,(VectQuot (V,W)) st

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

let W be Subspace of V; :: thesis: ex QL being LinearOperator of V,(VectQuot (V,W)) st

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

defpred S_{1}[ VECTOR of V, object ] means $2 = $1 + W;

A1: for x being Element of the carrier of V ex y being Element of the carrier of (VectQuot (V,W)) st S_{1}[x,y]

A2: for x being Element of V holds S_{1}[x,QL . x]
from FUNCT_2:sch 3(A1);

A3: for v, w being Element of V holds QL . (v + w) = (QL . v) + (QL . w)

for r being Real holds QL . (r * v) = r * (QL . v)

then reconsider QL = QL as LinearOperator of V,(VectQuot (V,W)) ;

take QL ; :: thesis: ( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

for v being object st v in the carrier of (VectQuot (V,W)) holds

ex s being object st

( s in the carrier of V & v = QL . s )

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

let W be Subspace of V; :: thesis: ex QL being LinearOperator of V,(VectQuot (V,W)) st

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

defpred S

A1: for x being Element of the carrier of V ex y being Element of the carrier of (VectQuot (V,W)) st S

proof

consider QL being Function of the carrier of V,(VectQuot (V,W)) such that
let x be Element of the carrier of V; :: thesis: ex y being Element of the carrier of (VectQuot (V,W)) st S_{1}[x,y]

reconsider v = x + W as Point of (VectQuot (V,W)) by LMQ07;

take v ; :: thesis: S_{1}[x,v]

thus S_{1}[x,v]
; :: thesis: verum

end;reconsider v = x + W as Point of (VectQuot (V,W)) by LMQ07;

take v ; :: thesis: S

thus S

A2: for x being Element of V holds S

A3: for v, w being Element of V holds QL . (v + w) = (QL . v) + (QL . w)

proof

for v being VECTOR of V
let v, w be Element of V; :: thesis: QL . (v + w) = (QL . v) + (QL . w)

A4: QL . v = v + W by A2;

A5: QL . w = w + W by A2;

thus QL . (v + w) = (v + w) + W by A2

.= (QL . v) + (QL . w) by A4, A5, LMQ11 ; :: thesis: verum

end;A4: QL . v = v + W by A2;

A5: QL . w = w + W by A2;

thus QL . (v + w) = (v + w) + W by A2

.= (QL . v) + (QL . w) by A4, A5, LMQ11 ; :: thesis: verum

for r being Real holds QL . (r * v) = r * (QL . v)

proof

then
( QL is additive & QL is homogeneous )
by A3, LOPBAN_1:def 5;
let v be VECTOR of V; :: thesis: for r being Real holds QL . (r * v) = r * (QL . v)

let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

A6: QL . v = v + W by A2;

thus QL . (r * v) = (r * v) + W by A2

.= r * (QL . v) by A6, LMQ09 ; :: thesis: verum

end;let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

A6: QL . v = v + W by A2;

thus QL . (r * v) = (r * v) + W by A2

.= r * (QL . v) by A6, LMQ09 ; :: thesis: verum

then reconsider QL = QL as LinearOperator of V,(VectQuot (V,W)) ;

take QL ; :: thesis: ( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

for v being object st v in the carrier of (VectQuot (V,W)) holds

ex s being object st

( s in the carrier of V & v = QL . s )

proof

hence
( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )
by A2, FUNCT_2:10; :: thesis: verum
let v be object ; :: thesis: ( v in the carrier of (VectQuot (V,W)) implies ex s being object st

( s in the carrier of V & v = QL . s ) )

assume v in the carrier of (VectQuot (V,W)) ; :: thesis: ex s being object st

( s in the carrier of V & v = QL . s )

then reconsider v1 = v as Point of (VectQuot (V,W)) ;

consider s being VECTOR of V such that

A7: v1 = s + W by LMQ07;

take s ; :: thesis: ( s in the carrier of V & v = QL . s )

thus s in the carrier of V ; :: thesis: v = QL . s

thus v = QL . s by A2, A7; :: thesis: verum

end;( s in the carrier of V & v = QL . s ) )

assume v in the carrier of (VectQuot (V,W)) ; :: thesis: ex s being object st

( s in the carrier of V & v = QL . s )

then reconsider v1 = v as Point of (VectQuot (V,W)) ;

consider s being VECTOR of V such that

A7: v1 = s + W by LMQ07;

take s ; :: thesis: ( s in the carrier of V & v = QL . s )

thus s in the carrier of V ; :: thesis: v = QL . s

thus v = QL . s by A2, A7; :: thesis: verum