let n be Nat; :: thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
let p1, p2, p3 be Element of n -tuples_on REAL; :: thesis: |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
reconsider f1 = p1, f2 = p2, f3 = p3 as real-valued FinSequence ;
len f2 = n by CARD_1:def 7;
then ( len f1 = len f2 & len f2 = len f3 ) by CARD_1:def 7;
hence |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| by Th120; :: thesis: verum