let x, y, z be ExtReal; :: thesis: ( 0 <= x & 0 <= y & 0 <= z implies (x + y) + z = x + (y + z) )
assume that
A1: 0 <= x and
A2: 0 <= y and
A3: 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 A1, A2, A3, XXREAL_0:14;

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

then consider a, b, c, d, e being Real such that
A4: ( x = a & y = b & z = c ) and
x + y = d and
y + z = e ;
(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)

then (x + y) + z = +infty + z by A2, Def2
.= +infty by A3, Def2
.= +infty + (y + z) by A2, A3, Def2 ;
hence (x + y) + z = x + (y + z) by A5; :: thesis: verum

end;

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

then (x + y) + z = +infty + z by A1, Def2
.= +infty by A3, Def2
.= x + +infty by A1, Def2
.= x + (+infty + z) by A3, Def2 ;
hence (x + y) + z = x + (y + z) by A6; :: thesis: verum

end;

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

then (x + y) + z = +infty by A1, A2, Def2
.= x + +infty by A1, Def2
.= x + (y + +infty) by A2, Def2 ;
hence (x + y) + z = x + (y + z) by A7; :: thesis: verum

end;

end;