let n be Nat; 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; |((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)|
; verum