let D1, D2 be non empty set ; :: thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
let f2 be BinOp of D2; :: thesis: ( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
defpred S₁[ set , set ] means |:f1,f2:| . ($1,$2) = |:f1,f2:| . ($2,$1);
thus ( f1 is commutative & f2 is commutative implies |:f1,f2:| is commutative ) :: thesis: ( |:f1,f2:| is commutative implies ( f1 is commutative & f2 is commutative ) )

proof

assume A1: for a, b being Element of D1 holds f1 . (a,b) = f1 . (b,a) ; :: according to BINOP_1:def 2 :: thesis: ( not f2 is commutative or |:f1,f2:| is commutative )
assume A2: for a, b being Element of D2 holds f2 . (a,b) = f2 . (b,a) ; :: according to BINOP_1:def 2 :: thesis: |:f1,f2:| is commutative
A3: for d1, d19 being Element of D1
for d2, d29 being Element of D2 holds S₁[[d1,d2],[d19,d29]]

proof

let a1, b1 be Element of D1; :: thesis: for d2, d29 being Element of D2 holds S₁[[a1,d2],[b1,d29]]
let a2, b2 be Element of D2; :: thesis: S₁[[a1,a2],[b1,b2]]
thus |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))] by Th21
.= [(f1 . (b1,a1)),(f2 . (a2,b2))] by A1
.= [(f1 . (b1,a1)),(f2 . (b2,a2))] by A2
.= |:f1,f2:| . ([b1,b2],[a1,a2]) by Th21 ; :: thesis: verum

end;

thus for a, b being Element of [:D1,D2:] holds S₁[a,b] from FILTER_1:sch 5(A3); :: according to BINOP_1:def 2 :: thesis: verum

end;

assume A4: for a, b being Element of [:D1,D2:] holds |:f1,f2:| . (a,b) = |:f1,f2:| . (b,a) ; :: according to BINOP_1:def 2 :: thesis: ( f1 is commutative & f2 is commutative )
thus for a, b being Element of D1 holds f1 . (a,b) = f1 . (b,a) :: according to BINOP_1:def 2 :: thesis: f2 is commutative

proof

set a2 = the Element of D2;
let a1, b1 be Element of D1; :: thesis: f1 . (a1,b1) = f1 . (b1,a1)
[(f1 . (a1,b1)),(f2 . ( the Element of D2, the Element of D2))] = |:f1,f2:| . ([a1, the Element of D2],[b1, the Element of D2]) by Th21
.= |:f1,f2:| . ([b1, the Element of D2],[a1, the Element of D2]) by A4
.= [(f1 . (b1,a1)),(f2 . ( the Element of D2, the Element of D2))] by Th21 ;
hence f1 . (a1,b1) = f1 . (b1,a1) by XTUPLE_0:1; :: thesis: verum

end;

set a1 = the Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def 2 :: thesis: for b₁ being Element of D2 holds f2 . (a2,b₁) = f2 . (b₁,a2)
let b2 be Element of D2; :: thesis: f2 . (a2,b2) = f2 . (b2,a2)
[(f1 . ( the Element of D1, the Element of D1)),(f2 . (a2,b2))] = |:f1,f2:| . ([ the Element of D1,a2],[ the Element of D1,b2]) by Th21
.= |:f1,f2:| . ([ the Element of D1,b2],[ the Element of D1,a2]) by A4
.= [(f1 . ( the Element of D1, the Element of D1)),(f2 . (b2,a2))] by Th21 ;
hence f2 . (a2,b2) = f2 . (b2,a2) by XTUPLE_0:1; :: thesis: verum