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)

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

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

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

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