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