let a be Domain-Sequence; :: thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative
let b be BinOps of a; :: thesis: ( ( for i being Element of dom a holds b . i is commutative ) implies [:b:] is commutative )
assume A1: for i being Element of dom a holds b . i is commutative ; :: thesis: [:b:] is commutative
let x, y be Element of product a; :: according to BINOP_1:def 2 :: thesis: [:b:] . (x,y) = [:b:] . (y,x)

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

let z be object ; :: thesis: ( z in dom a implies ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z )
assume z in dom a ; :: thesis: ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z
then reconsider i = z as Element of dom a ;
A3: ([:b:] . (y,x)) . i = (b . i) . ((y . i),(x . i)) by Def8;
( b . i is commutative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z by A3; :: thesis: verum

end;

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