let x, y, z be ext-real number ; :: thesis: ( 0 <= x & 0 <= y & 0 <= z implies (x + y) + z = x + (y + z) )
assume Z: ( 0 <= x & 0 <= y & 0 <= z ) ; :: thesis: (x + y) + z = x + (y + z)

per cases ( ( x in REAL & y in REAL & z in REAL ) or x = +infty or y = +infty or z = +infty ) by Z, XXREAL_0:14;

suppose A3: ( x in REAL & y in REAL & z in REAL ) ; :: thesis: (x + y) + z = x + (y + z)

consider a, b, c, d, e being real number such that
A4: ( x = a & y = b & z = c & x + y = d & y + z = e ) by A3;
(x + y) + z = (a + b) + c by A4
.= a + (b + c)
.= x + (y + z) by A4 ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum

end;

suppose A5: x = +infty ; :: thesis: (x + y) + z = x + (y + z)

(x + y) + z = +infty + z by A5, Def3, Z
.= +infty by Def3, Z
.= +infty + (y + z) by Z, Def3 ;
hence (x + y) + z = x + (y + z) by A5; :: thesis: verum

end;

suppose A7: y = +infty ; :: thesis: (x + y) + z = x + (y + z)

then (x + y) + z = +infty + z by Def3, Z
.= +infty by Def3, Z
.= x + +infty by Def3, Z
.= x + (+infty + z) by Def3, Z ;
hence (x + y) + z = x + (y + z) by A7; :: thesis: verum

end;

suppose A8: z = +infty ; :: thesis: (x + y) + z = x + (y + z)

(x + y) + z = +infty by A8, Def3, Z
.= x + +infty by Def3, Z
.= x + (y + +infty ) by Def3, Z ;
hence (x + y) + z = x + (y + z) by A8; :: thesis: verum

end;

end;