let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for W being Subspace of V st u in v + W holds
v + W = u + W
let u, v be VECTOR of V; :: thesis: for W being Subspace of V st u in v + W holds
v + W = u + W
let W be Subspace of V; :: thesis: ( u in v + W implies v + W = u + W )
reconsider C = v + W as Coset of W by RLSUB_1:def 6;
assume u in v + W ; :: thesis: v + W = u + W
then C = u + W by RLSUB_1:78;
hence v + W = u + W ; :: thesis: verum