let x1, x2, y1, y2 be real-valued FinSequence; :: thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y1 and
A3: len y1 = len y2 ; :: thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
|((x1 + x2),y2)| = |(x1,y2)| + |(x2,y2)| by A1, A2, A3, Th120;
then A4: |((x1 + x2),y1)| + |((x1 + x2),y2)| = (|(x1,y1)| + |(x2,y1)|) + (|(x1,y2)| + |(x2,y2)|) by A1, A2, Th120;
len (x1 + x2) = len x1 by A1, Th115;
hence |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| by A1, A2, A3, A4, Th120; :: thesis: verum