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