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₁[ 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₁[x,y]

proof

let x be Element of the carrier of V; :: thesis: ex y being Element of the carrier of (VectQuot (V,W)) st S₁[x,y]
reconsider v = x + W as Point of (VectQuot (V,W)) by LMQ07;
take v ; :: thesis: S₁[x,v]
thus S₁[x,v] ; :: thesis: verum

end;

consider QL being Function of the carrier of V,(VectQuot (V,W)) such that
A2: for x being Element of V holds S₁[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)

proof

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;

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

proof

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;

then ( QL is additive & QL is homogeneous ) by A3, LOPBAN_1:def 5;
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

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;

hence ( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) ) by A2, FUNCT_2:10; :: thesis: verum