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 3 :: thesis: [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z)

A2: now :: thesis: for v being object st v in dom a holds
([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v

set xy = [:b:] . (x,y);
set yz = [:b:] . (y,z);
let v be object ; :: 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)) . v
then reconsider i = v as Element of dom a ;
A3: ( ([:b:] . (y,z)) . i = (b . i) . ((y . i),(z . i)) & ([:b:] . (x,([:b:] . (y,z)))) . i = (b . i) . ((x . i),(([:b:] . (y,z)) . i)) ) by Def8;
A4: ([:b:] . (([:b:] . (x,y)),z)) . i = (b . i) . ((([:b:] . (x,y)) . i),(z . i)) by Def8;
( b . i is associative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v by A3, A4; :: thesis: verum

end;

( dom ([:b:] . (x,([:b:] . (y,z)))) = dom a & dom ([:b:] . (([:b:] . (x,y)),z)) = dom a ) by CARD_3:9;
hence [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z) by A2, FUNCT_1:2; :: thesis: verum