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 A2: ( p1 = r1 & p2 = r2 ) ; :: thesis: p1 + p2 = r1 + r2
reconsider s1 = r1, s2 = r2 as Element of REAL n by A2, EUCLID:22;
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 EUCLID:def 8;
then XX: the addF of (TOP-REAL n) = the addF of RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def 6
.= RealFuncAdd (Seg n) ;
reconsider f = s1, g = s2 as Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
thus p1 + p2 = (RealFuncAdd (Seg n)) . (r1,r2) by A2, XX, ALGSTR_0:def 1
.= addreal .: (f,g) by FUNCSDOM:def 1
.= s1 + s2 by RVSUM_1:def 4
.= r1 + r2 ; :: thesis: verum