let x1, x2, y1, y2 be FinSequence of COMPLEX ; :: 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 A1: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 ) ; :: thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
then |((x1 + x2),y2)| = |(x1,y2)| + |(x2,y2)| by Th66;
then A2: |((x1 + x2),y1)| + |((x1 + x2),y2)| = (|(x1,y1)| + |(x2,y1)|) + (|(x1,y2)| + |(x2,y2)|) by A1, Th66;
len (x1 + x2) = len x1 by A1, Th6;
hence |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| by A1, A2, Th71; :: thesis: verum