for r being Element of ExtREAL holds multextreal . (r,1.) = r

proof

let r be Element of ExtREAL ; :: thesis: multextreal . (r,1.) = r
multextreal . (r,1.) = r * 1. by Def1;
hence multextreal . (r,1.) = r by XXREAL_3:81; :: thesis: verum

end;

then A1: 1. is_a_right_unity_wrt multextreal by BINOP_1:def 6;
for r being Element of ExtREAL holds multextreal . (1.,r) = r

proof

let r be Element of ExtREAL ; :: thesis: multextreal . (1.,r) = r
multextreal . (1.,r) = 1. * r by Def1;
hence multextreal . (1.,r) = r by XXREAL_3:81; :: thesis: verum

end;

then 1. is_a_left_unity_wrt multextreal by BINOP_1:def 5;
hence 1. is_a_unity_wrt multextreal by A1, BINOP_1:def 7; :: thesis: verum