let x be R_eal; :: thesis: ( 1. * x = x & (R_EAL 1) * x = x )
A1: R_EAL 1 = 1. by MEASURE6:def 1, MESFUNC1:def 8;

per cases ( x is Real or x = +infty or x = -infty ) by XXREAL_0:14;

suppose x is Real ; :: thesis: ( 1. * x = x & (R_EAL 1) * x = x )

then reconsider a = x as Real ;
1. * x = 1 * a by EXTREAL1:13, MESFUNC1:def 8;
hence ( 1. * x = x & (R_EAL 1) * x = x ) by MEASURE6:def 1, MESFUNC1:def 8; :: thesis: verum

end;

suppose x = +infty ; :: thesis: ( 1. * x = x & (R_EAL 1) * x = x )

hence ( 1. * x = x & (R_EAL 1) * x = x ) by A1, EXTREAL1:def 1, MESFUNC1:def 8; :: thesis: verum

end;

suppose x = -infty ; :: thesis: ( 1. * x = x & (R_EAL 1) * x = x )

hence ( 1. * x = x & (R_EAL 1) * x = x ) by A1, EXTREAL1:def 1, MESFUNC1:def 8; :: thesis: verum

end;

end;