let a be Domain-Sequence; :: thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative
let b be BinOps of a; :: thesis: ( ( for i being Element of dom a holds b . i is associative ) implies [:b:] is associative )
assume A1:
for i being Element of dom a holds b . i is associative
; :: thesis: [:b:] is associative
let x, y, z be Element of product a; :: according to BINOP_1:def 14 :: thesis: [:b:] . x,([:b:] . y,z) = [:b:] . ([:b:] . x,y),z
A2:
( dom ([:b:] . x,([:b:] . y,z)) = dom a & dom ([:b:] . ([:b:] . x,y),z) = dom a )
by CARD_3:18;
now let v be
set ;
:: thesis: ( v in dom a implies ([:b:] . x,([:b:] . y,z)) . v = ([:b:] . ([:b:] . x,y),z) . v )assume
v in dom a
;
:: thesis: ([:b:] . x,([:b:] . y,z)) . v = ([:b:] . ([:b:] . x,y),z) . vthen reconsider i =
v as
Element of
dom a ;
set xy =
[:b:] . x,
y;
set yz =
[:b:] . y,
z;
(
b . i is
associative &
([:b:] . x,y) . i = (b . i) . (x . i),
(y . i) &
([:b:] . y,z) . i = (b . i) . (y . i),
(z . i) &
([:b:] . x,([:b:] . y,z)) . i = (b . i) . (x . i),
(([:b:] . y,z) . i) &
([:b:] . ([:b:] . x,y),z) . i = (b . i) . (([:b:] . x,y) . i),
(z . i) )
by A1, Def10;
hence
([:b:] . x,([:b:] . y,z)) . v = ([:b:] . ([:b:] . x,y),z) . v
by BINOP_1:def 3;
:: thesis: verum end;
hence
[:b:] . x,([:b:] . y,z) = [:b:] . ([:b:] . x,y),z
by A2, FUNCT_1:9; :: thesis: verum