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

now

let z be set ; :: 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 ;
( b . i is commutative & ([:b:] . x,y) . i = (b . i) . (x . i),(y . i) & ([:b:] . y,x) . i = (b . i) . (y . i),(x . i) ) by A1, Def10;
hence ([:b:] . x,y) . z = ([:b:] . y,x) . z by BINOP_1:def 2; :: thesis: verum

end;

hence [:b:] . x,y = [:b:] . y,x by A2, FUNCT_1:9; :: thesis: verum