let y, z be ExtReal; :: thesis: ( 0 <= y & y < +infty implies z = (z + y) - y )
assume ( 0 <= y & y < +infty ) ; :: thesis: z = (z + y) - y
then y in REAL by XXREAL_0:14;
hence z = (z + y) - y by Th22; :: thesis: verum