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

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

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 V1 + W1 or x in V + W )
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;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

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