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
A1: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
let r1, r2 be real-valued Function; :: thesis: ( p1 = r1 & p2 = r2 implies p1 + p2 = r1 + r2 )
assume A2: ( p1 = r1 & p2 = r2 ) ; :: thesis: p1 + p2 = r1 + r2
reconsider s1 = r1, s2 = r2 as Element of REAL n by A2, Th19;
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;
hence p1 + p2 = (RealFuncAdd (Seg n)) . (r1,r2) by A2, ALGSTR_0:def 1
.= s1 + s2 by A1, FUNCSDOM:def 1
.= r1 + r2 ;
:: thesis: verum