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

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 (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;

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 (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