let V be RealLinearSpace; :: thesis:
let W be Subspace of V; :: thesis:
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]

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

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)

let v, w be Element of V; :: thesis:
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:

end;

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

let v be VECTOR of V; :: thesis:
let r be Real; :: thesis:
A6: QL . v = v + W by A2;
thus QL . (r * v) = (r * v) + W by A2
.= r * (QL . v) by A6, LMQ09 ; :: thesis:

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:
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 )

let v be object ; :: thesis:
assume v in the carrier of (VectQuot (V,W)) ; :: thesis:
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:
thus s in the carrier of V ; :: thesis:
thus v = QL . s by A2, A7; :: thesis:

end;

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