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 ;
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;
verum
end;
for a, b being Element of ExtREAL holds multextreal . (a,b) = multextreal . (b,a)
hence
( multextreal is commutative & multextreal is associative )
by A1, BINOP_1:def 2, BINOP_1:def 3; verum