let V be RealUnitarySpace; :: 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 object st x in v + M holds
x in v + W

proof

let x be object ; :: 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
A2: x = v + u and
A3: u in M ;
u in W by A1, A3;
then x in { (v + u9) where u9 is VECTOR of V : u9 in W } by A2;
hence x in v + W by RUSUB_1:def 4; :: thesis: verum

end;

then A4: v + M c= v + W ;
for x being object st x in v + W holds
x in v + M

proof

let x be object ; :: 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 RUSUB_1:def 4;
then consider u being VECTOR of V such that
A5: x = v + u and
A6: u in W ;
u in M by A1, A6;
hence x in v + M by A5; :: thesis: verum

end;

then v + W c= v + M ;
hence v + W = v + M by A4; :: thesis: verum