let x1, x2, x3 be real-valued FinSequence; :: thesis: ( len x1 = len x2 & len x2 = len x3 implies |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len x3 ; :: thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
len (- x2) = len x2 by Th114;
then |((x1 - x2),x3)| = |(x1,x3)| + |((- x2),x3)| by A1, A2, Th120
.= |(x1,x3)| + (- |(x2,x3)|) by A2, Th122 ;
hence |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| ; :: thesis: verum