let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
let p1, p2 be Point of (TOP-REAL n); :: thesis: for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
let r1, r2 be real-valued Function; :: thesis: ( p1 = r1 & p2 = r2 implies p1 + p2 = r1 + r2 )
assume Z1: ( p1 = r1 & p2 = r2 ) ; :: thesis: p1 + p2 = r1 + r2
X1: 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) #) = RealVectSpace (Seg n) by Def8;
X2: REAL n = Funcs (Seg n),REAL by FINSEQ_2:111;
reconsider s1 = r1, s2 = r2 as Element of REAL n by Z1, Th25;
thus p1 + p2 = (RealFuncAdd (Seg n)) . r1,r2 by Z1, X1, ALGSTR_0:def 1
.= s1 + s2 by Z1, X2, FUNCSDOM:def 2
.= r1 + r2 ; :: thesis: verum