let V be RealLinearSpace; :: thesis: for W being Subspace of V
for x being object holds
( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )
let W be Subspace of V; :: thesis: for x being object holds
( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )
let x be object ; :: thesis: ( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )
A1: ( x in the carrier of (VectQuot (V,W)) iff x in CosetSet (V,W) ) by LMQ06;
( ex A being Coset of W st x = A iff ex v being Point of V st x = v + W )

proof

thus ( ex A being Coset of W st x = A implies ex v being Point of V st x = v + W ) by RLSUB_1:def 6; :: thesis: ( ex v being Point of V st x = v + W implies ex A being Coset of W st x = A )
assume ex v being Point of V st x = v + W ; :: thesis: ex A being Coset of W st x = A
then x is Coset of W by RLSUB_1:def 6;
hence ex A being Coset of W st x = A ; :: thesis: verum

end;

hence ( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W ) by A1; :: thesis: verum