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

for x being object st x in v + W holds

x in v + M

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

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

then A4:
v + M c= v + W
;
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;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

for x being object st x in v + W holds

x in v + M

proof

then
v + W c= v + M
;
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;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

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