let n be Nat; :: thesis: for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
let x1, x2, y1, y2 be Element of REAL n; :: thesis: |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
thus |((x1 - x2),(y1 - y2))| = |(x1,(y1 - y2))| - |(x2,(y1 - y2))| by Th26
.= (|(x1,y1)| - |(x1,y2)|) - |(x2,(y1 - y2))| by Th26
.= (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by Th26
.= ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| ; :: thesis: verum