let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); :: thesis: for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|
let x be Real; :: thesis: |((x * p1),p2)| = x * |(p1,p2)|
reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1 as Element of REAL n by EUCLID:22;
( len f1 = n & len f2 = n ) by CARD_1:def 7;
hence |((x * p1),p2)| = x * |(p1,p2)| by RVSUM_1:121; :: thesis: verum