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 Th20
.= (|(x1,y1)| + |(x1,y2)|) + |(x2,(y1 + y2))| by Th20
.= (|(x1,y1)| + |(x1,y2)|) + (|(x2,y1)| + |(x2,y2)|) by Th20
.= ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| ; :: thesis: verum