let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); :: thesis: for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let x be real number ; :: thesis: |((x * p1),p2)| = x * |(p1,p2)|
reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:27;
reconsider q1 = p1 as Element of REAL n by EUCLID:25;
A1: x * p1 = x * q1 by EUCLID:69;
( len f1 = n & len f2 = n ) by FINSEQ_1:def 18;
hence |((x * p1),p2)| = x * |(p1,p2)| by A1, RVSUM_1:151; :: thesis: verum