let n be Nat; :: thesis: for p being Element of (TOP-REAL n)
for f being Element of (REAL-NS n)
for H being Subset of (TOP-REAL n)
for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I
let p be Element of (TOP-REAL n); :: thesis: for f being Element of (REAL-NS n)
for H being Subset of (TOP-REAL n)
for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I
let f be Element of (REAL-NS n); :: thesis: for H being Subset of (TOP-REAL n)
for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I
let H be Subset of (TOP-REAL n); :: thesis: for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I
let I be Subset of (REAL-NS n); :: thesis: ( p = f & H = I implies p + H = f + I )
assume A1: ( p = f & H = I ) ; :: thesis: p + H = f + I
for x being object holds
( x in p + H iff x in f + I )

proof

let x be object ; :: thesis: ( x in p + H iff x in f + I )

hereby :: thesis: ( x in f + I implies x in p + H )

assume x in p + H ; :: thesis: x in f + I
then consider v being Element of (TOP-REAL n) such that
A2: ( x = p + v & v in H ) ;
reconsider w = v as Element of (REAL-NS n) by Th4;
x = f + w by A1, A2, Th7;
hence x in f + I by A2, A1; :: thesis: verum

end;

assume x in f + I ; :: thesis: x in p + H
then consider v being Element of (REAL-NS n) such that
A3: ( x = f + v & v in I ) ;
reconsider w = v as Element of (TOP-REAL n) by Th4;
x = p + w by A1, A3, Th7;
hence x in p + H by A1, A3; :: thesis: verum

end;

hence p + H = f + I by TARSKI:2; :: thesis: verum