let X be RealNormSpace; :: thesis: for V being Subset of X

for x being Point of X

for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let V be Subset of X; :: thesis: for x being Point of X

for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let x be Point of X; :: thesis: for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let V1 be Subset of (LinearTopSpaceNorm X); :: thesis: for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let x1 be Point of (LinearTopSpaceNorm X); :: thesis: ( V = V1 & x = x1 implies x + V = x1 + V1 )

assume that

A1: V = V1 and

A2: x = x1 ; :: thesis: x + V = x1 + V1

thus x + V c= x1 + V1 :: according to XBOOLE_0:def 10 :: thesis: x1 + V1 c= x + V

assume z in x1 + V1 ; :: thesis: z in x + V

then consider u1 being Point of (LinearTopSpaceNorm X) such that

A5: z = x1 + u1 and

A6: u1 in V1 ;

reconsider u = u1 as Point of X by A1, A6;

x1 + u1 = x + u by A2, NORMSP_2:def 4;

hence z in x + V by A1, A5, A6; :: thesis: verum

for x being Point of X

for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let V be Subset of X; :: thesis: for x being Point of X

for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let x be Point of X; :: thesis: for V1 being Subset of (LinearTopSpaceNorm X)

for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let V1 be Subset of (LinearTopSpaceNorm X); :: thesis: for x1 being Point of (LinearTopSpaceNorm X) st V = V1 & x = x1 holds

x + V = x1 + V1

let x1 be Point of (LinearTopSpaceNorm X); :: thesis: ( V = V1 & x = x1 implies x + V = x1 + V1 )

assume that

A1: V = V1 and

A2: x = x1 ; :: thesis: x + V = x1 + V1

thus x + V c= x1 + V1 :: according to XBOOLE_0:def 10 :: thesis: x1 + V1 c= x + V

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x1 + V1 or z in x + V )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x + V or z in x1 + V1 )

assume z in x + V ; :: thesis: z in x1 + V1

then consider u being Point of X such that

A3: z = x + u and

A4: u in V ;

reconsider u1 = u as Point of (LinearTopSpaceNorm X) by A1, A4;

x + u = x1 + u1 by A2, NORMSP_2:def 4;

hence z in x1 + V1 by A1, A3, A4; :: thesis: verum

end;assume z in x + V ; :: thesis: z in x1 + V1

then consider u being Point of X such that

A3: z = x + u and

A4: u in V ;

reconsider u1 = u as Point of (LinearTopSpaceNorm X) by A1, A4;

x + u = x1 + u1 by A2, NORMSP_2:def 4;

hence z in x1 + V1 by A1, A3, A4; :: thesis: verum

assume z in x1 + V1 ; :: thesis: z in x + V

then consider u1 being Point of (LinearTopSpaceNorm X) such that

A5: z = x1 + u1 and

A6: u1 in V1 ;

reconsider u = u1 as Point of X by A1, A6;

x1 + u1 = x + u by A2, NORMSP_2:def 4;

hence z in x + V by A1, A5, A6; :: thesis: verum