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,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by Th72;
then A2: |(x1,(y1 - y2))| - |(x2,(y1 - y2))| = (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by A1, Th72;
len (y1 - y2) = len y1 by A1, Th7;
hence |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| by A1, A2, Th70; :: thesis: verum