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 Def2;
hence multextreal . 1. ,r = r by XXREAL_3:92; :: thesis: verum

end;

then A1: 1. is_a_left_unity_wrt multextreal by BINOP_1:def 5;
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 Def2;
hence multextreal . r,1. = r by XXREAL_3:92; :: thesis: verum

end;

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