let a, b be real number ; :: thesis: ( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
reconsider a9 = a, b9 = b, c9 = a + b as Real by XREAL_0:def 1;
A1: b9 = R_EAL b ;
A2: a9 = R_EAL a ;
hence (R_EAL a) + (R_EAL b) = a + b by A1, SUPINF_2:1; :: thesis: ( - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
- a9 = R_EAL (- a) ;
hence - (R_EAL a) = - a by SUPINF_2:3; :: thesis: ( (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
thus (R_EAL a) - (R_EAL b) = a - b by A2, A1, SUPINF_2:5; :: thesis: (R_EAL a) * (R_EAL b) = a * b
thus (R_EAL a) * (R_EAL b) = a * b by A2, A1, EXTREAL1:13; :: thesis: verum