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 S1[ 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 S1[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 S1[x,y]
reconsider v = x + W as Point of (VectQuot (V,W)) by LMQ07;
take v ; :: thesis: S1[x,v]
thus S1[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 S1[x,QL . x] from 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 ; :: 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 ; :: thesis: verum
end;
then ( QL is additive & QL is homogeneous ) by ;
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 ; :: thesis: verum