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: now

set xy = [:b:] . x,y;
set yz = [:b:] . y,z;
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) . 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 Def10;
A4: ([:b:] . ([:b:] . x,y),z) . i = (b . i) . (([:b:] . x,y) . i),(z . i) by Def10;
( b . i is associative & ([:b:] . x,y) . i = (b . i) . (x . i),(y . i) ) by A1, Def10;
hence ([:b:] . x,([:b:] . y,z)) . v = ([:b:] . ([:b:] . x,y),z) . v by A3, A4, BINOP_1:def 3; :: thesis: verum

end;

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