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
thus p + q = the addF of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) . (p,q)
.= the addF of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) . (p,q) by Th1
.= f + g by A1 ; :: thesis: verum