let V be RealLinearSpace; :: thesis: for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let W be strict Subspace of V; :: thesis: for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let M be Subset of V; :: thesis: for v being VECTOR of V st Up W = M holds
v + W = v + M
let v be VECTOR of V; :: thesis: ( Up W = M implies v + W = v + M )
assume A1: Up W = M ; :: thesis: v + W = v + M
for x being set st x in v + W holds
x in v + M

proof

let x be set ; :: thesis: ( x in v + W implies x in v + M )
assume x in v + W ; :: thesis: x in v + M
then x in { (v + u) where u is VECTOR of V : u in W } by RLSUB_1:def 5;
then consider u being VECTOR of V such that
A2: ( x = v + u & u in W ) ;
u in M by A1, A2, STRUCT_0:def 5;
hence x in v + M by A2; :: thesis: verum

end;

then A3: v + W c= v + M by TARSKI:def 3;
for x being set st x in v + M holds
x in v + W

proof

let x be set ; :: thesis: ( x in v + M implies x in v + W )
assume x in v + M ; :: thesis: x in v + W
then consider u being Element of V such that
A4: ( x = v + u & u in M ) ;
u in W by A1, A4, STRUCT_0:def 5;
then x in { (v + u') where u' is VECTOR of V : u' in W } by A4;
hence x in v + W by RLSUB_1:def 5; :: thesis: verum

end;

then v + M c= v + W by TARSKI:def 3;
hence v + W = v + M by A3, XBOOLE_0:def 10; :: thesis: verum