let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let u, v be VECTOR of V; :: thesis: for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let W be Subspace of V; :: thesis: ( v in u + W iff u + W = v + W )
thus ( v in u + W implies u + W = v + W ) :: thesis: ( u + W = v + W implies v in u + W )

proof

assume v in u + W ; :: thesis: u + W = v + W
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W ;
thus u + W c= v + W :: according to XBOOLE_0:def 10 :: thesis: v + W c= u + W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in u + W or x in v + W )
assume x in u + W ; :: thesis: x in v + W
then consider v1 being VECTOR of V such that
A3: x = u + v1 and
A4: v1 in W ;
v - z = u + (z - z) by A1, RLVECT_1:def 3
.= u + (0. V) by RLVECT_1:15
.= u ;
then A5: x = v + (v1 + (- z)) by A3, RLVECT_1:def 3
.= v + (v1 - z) ;
v1 - z in W by A2, A4, Th23;
hence x in v + W by A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + W or x in u + W )
assume x in v + W ; :: thesis: x in u + W
then consider v2 being VECTOR of V such that
A6: ( x = v + v2 & v2 in W ) ;
( z + v2 in W & x = u + (z + v2) ) by A1, A2, A6, Th20, RLVECT_1:def 3;
hence x in u + W ; :: thesis: verum

end;

thus ( u + W = v + W implies v in u + W ) by Th43; :: thesis: verum