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

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