let V be RealLinearSpace; :: thesis: for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let u, v1, v2 be VECTOR of V; :: thesis: for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let W be Subspace of V; :: thesis: ( u in v1 + W & u in v2 + W implies v1 + W = v2 + W )
assume that
A1: u in v1 + W and
A2: u in v2 + W ; :: thesis: v1 + W = v2 + W
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus v1 + W c= v2 + W :: according to XBOOLE_0:def 10 :: thesis: v2 + W c= v1 + W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v1 + W or x in v2 + W )
assume x in v1 + W ; :: thesis: x in v2 + W
then consider u1 being VECTOR of V such that
A7: x = v1 + u1 and
A8: u1 in W ;
x2 - x1 in W by A4, A6, Th23;
then A9: (x2 - x1) + u1 in W by A8, Th20;
u - x1 = v1 + (x1 - x1) by A3, RLVECT_1:def 3
.= v1 + (0. V) by RLVECT_1:15
.= v1 ;
then x = (v2 + (x2 - x1)) + u1 by A5, A7, RLVECT_1:def 3
.= v2 + ((x2 - x1) + u1) by RLVECT_1:def 3 ;
hence x in v2 + W by A9; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v2 + W or x in v1 + W )
assume x in v2 + W ; :: thesis: x in v1 + W
then consider u1 being VECTOR of V such that
A10: x = v2 + u1 and
A11: u1 in W ;
x1 - x2 in W by A4, A6, Th23;
then A12: (x1 - x2) + u1 in W by A11, Th20;
u - x2 = v2 + (x2 - x2) by A5, RLVECT_1:def 3
.= v2 + (0. V) by RLVECT_1:15
.= v2 ;
then x = (v1 + (x1 - x2)) + u1 by A3, A10, RLVECT_1:def 3
.= v1 + ((x1 - x2) + u1) by RLVECT_1:def 3 ;
hence x in v1 + W by A12; :: thesis: verum