let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|
let x1, x2, x3 be Element of REAL n; :: thesis: |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|
A1: len x3 = n by FINSEQ_1:def 18;
( len x1 = n & len x2 = n ) by FINSEQ_1:def 18;
hence |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)| by A1, RVSUM_1:150; :: thesis: verum