let n, k be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds

(p1 + p2) . k = (p1 . k) + (p2 . k)

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) )

A1: dom (p1 + p2) = Seg n by FINSEQ_1:89;

thus ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) ) by A1, VALUED_1:def 1; :: thesis: verum

(p1 + p2) . k = (p1 . k) + (p2 . k)

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) )

A1: dom (p1 + p2) = Seg n by FINSEQ_1:89;

thus ( k in Seg n implies (p1 + p2) . k = (p1 . k) + (p2 . k) ) by A1, VALUED_1:def 1; :: thesis: verum