let n be Nat; :: thesis: for p, q being Element of (TOP-REAL n)
for f, g being Element of (REAL-NS n) st p = f & q = g holds
p - q = f - g
let p, q be Element of (TOP-REAL n); :: thesis: for f, g being Element of (REAL-NS n) st p = f & q = g holds
p - q = f - g
let f, g be Element of (REAL-NS n); :: thesis: ( p = f & q = g implies p - q = f - g )
assume A1: ( p = f & q = g ) ; :: thesis: p - q = f - g
then - q = - g by Th9;
hence p - q = f - g by A1, Th7; :: thesis: verum