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)

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

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

( dom ([:b:] . (x,([:b:] . (y,z)))) = dom a & dom ([:b:] . (([:b:] . (x,y)),z)) = dom a )
by CARD_3:9;([: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;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

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