let X be RealNormSpace; :: thesis: for V, W being Subset of X
for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 & W = W1 holds
V + W = V1 + W1
let V, W be Subset of X; :: thesis: for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 & W = W1 holds
V + W = V1 + W1
let V1, W1 be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = V1 & W = W1 implies V + W = V1 + W1 )
assume that
A1: V = V1 and
A2: W = W1 ; :: thesis: V + W = V1 + W1
thus V + W c= V1 + W1 :: according to XBOOLE_0:def 10 :: thesis: V1 + W1 c= V + W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V + W or x in V1 + W1 )
assume x in V + W ; :: thesis: x in V1 + W1
then consider u, v being Point of X such that
A3: x = u + v and
A4: u in V and
A5: v in W ;
reconsider v1 = v as Point of (LinearTopSpaceNorm X) by A2, A5;
reconsider u1 = u as Point of (LinearTopSpaceNorm X) by A1, A4;
u + v = u1 + v1 by NORMSP_2:def 4;
hence x in V1 + W1 by A1, A2, A3, A4, A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V1 + W1 or x in V + W )
assume x in V1 + W1 ; :: thesis: x in V + W
then consider u, v being Point of (LinearTopSpaceNorm X) such that
A6: x = u + v and
A7: u in V1 and
A8: v in W1 ;
reconsider v1 = v as Point of X by A2, A8;
reconsider u1 = u as Point of X by A1, A7;
u + v = u1 + v1 by NORMSP_2:def 4;
hence x in V + W by A1, A2, A6, A7, A8; :: thesis: verum