let X be RealNormSpace; :: thesis: for V being Subset of X
for x being Point of X
for V1 being Subset of
for x1 being Point of 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
for x1 being Point of st V = V1 & x = x1 holds
x + V = x1 + V1

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

let V1 be Subset of ; :: thesis: for x1 being Point of st V = V1 & x = x1 holds
x + V = x1 + V1

let x1 be Point of ; :: 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 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 by A1, A4;
x + u = x1 + u1 by ;
hence z in x1 + V1 by A1, A3, A4; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x1 + V1 or z in x + V )
assume z in x1 + V1 ; :: thesis: z in x + V
then consider u1 being Point of 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 ;
hence z in x + V by A1, A5, A6; :: thesis: verum