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 )
assume A1: u in v + W ; :: thesis: v + W = u + W
reconsider C = v + W as Coset of W by RLSUB_1:def 6;
C = u + W by A1, RLSUB_1:94;
hence v + W = u + W ; :: thesis: verum