A1: for a, b, c being Element of ExtREAL holds multextreal . a,(multextreal . b,c) = multextreal . (multextreal . a,b),c

proof

let a, b, c be Element of ExtREAL ; :: thesis: multextreal . a,(multextreal . b,c) = multextreal . (multextreal . a,b),c
multextreal . a,(multextreal . b,c) = multextreal . a,(b * c) by Def2;
then multextreal . a,(multextreal . b,c) = a * (b * c) by Def2;
then multextreal . a,(multextreal . b,c) = (a * b) * c by XXREAL_3:77;
then multextreal . a,(multextreal . b,c) = multextreal . (a * b),c by Def2;
hence multextreal . a,(multextreal . b,c) = multextreal . (multextreal . a,b),c by Def2; :: thesis: verum

end;

for a, b being Element of ExtREAL holds multextreal . a,b = multextreal . b,a

proof

let a, b be Element of ExtREAL ; :: thesis: multextreal . a,b = multextreal . b,a
multextreal . a,b = a * b by Def2;
hence multextreal . a,b = multextreal . b,a by Def2; :: thesis: verum

end;

hence ( multextreal is commutative & multextreal is associative ) by A1, BINOP_1:def 2, BINOP_1:def 3; :: thesis: verum