let V be RealLinearSpace; 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; 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; ( 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
; 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
XBOOLE_0:def 10 v2 + W c= v1 + W
let x be object ; TARSKI:def 3 ( not x in v2 + W or x in v1 + W )
assume
x in v2 + W
; 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; verum