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 Def1;
then multextreal . (a,(multextreal . (b,c))) = a * (b * c) by Def1;
then multextreal . (a,(multextreal . (b,c))) = (a * b) * c by XXREAL_3:66;
then multextreal . (a,(multextreal . (b,c))) = multextreal . ((a * b),c) by Def1;
hence multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c) by Def1; :: 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 Def1;
hence multextreal . (a,b) = multextreal . (b,a) by Def1; :: thesis: verum

end;

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