let n be Nat; :: thesis: for p1, p2 being Element of n -tuples_on REAL
for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|
let p1, p2 be Element of n -tuples_on REAL; :: 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 real-valued FinSequence ;
( len f1 = n & len f2 = n ) by CARD_1:def 7;
hence |((x * p1),p2)| = x * |(p1,p2)| by Th121; :: thesis: verum