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 )

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

hence
( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )
by A1; :: thesis: verum
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;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