let D1, D2 be non empty set ; :: thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
let f2 be BinOp of D2; :: thesis: ( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
thus ( f1 is associative & f2 is associative implies |:f1,f2:| is associative ) :: thesis: ( |:f1,f2:| is associative implies ( f1 is associative & f2 is associative ) )

proof

defpred S₁[ set , set , set ] means |:f1,f2:| . $1,(|:f1,f2:| . $2,$3) = |:f1,f2:| . (|:f1,f2:| . $1,$2),$3;
assume A1: for a, b, c being Element of D1 holds f1 . a,(f1 . b,c) = f1 . (f1 . a,b),c ; :: according to BINOP_1:def 14 :: thesis: ( not f2 is associative or |:f1,f2:| is associative )
assume A2: for a, b, c being Element of D2 holds f2 . a,(f2 . b,c) = f2 . (f2 . a,b),c ; :: according to BINOP_1:def 14 :: thesis: |:f1,f2:| is associative

A3: now

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

end;

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

end;

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

proof

consider a2, b2, c2 being Element of D2;
let a1, b1, c1 be Element of D1; :: thesis: f1 . a1,(f1 . b1,c1) = f1 . (f1 . a1,b1),c1
[(f1 . a1,(f1 . b1,c1)),(f2 . a2,(f2 . b2,c2))] = |:f1,f2:| . [a1,a2],[(f1 . b1,c1),(f2 . b2,c2)] by Th22
.= |:f1,f2:| . [a1,a2],(|:f1,f2:| . [b1,b2],[c1,c2]) by Th22
.= |:f1,f2:| . (|:f1,f2:| . [a1,a2],[b1,b2]),[c1,c2] by A4
.= |:f1,f2:| . [(f1 . a1,b1),(f2 . a2,b2)],[c1,c2] by Th22
.= [(f1 . (f1 . a1,b1),c1),(f2 . (f2 . a2,b2),c2)] by Th22 ;
hence f1 . a1,(f1 . b1,c1) = f1 . (f1 . a1,b1),c1 by ZFMISC_1:33; :: thesis: verum

end;

consider a1, b1, c1 being Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of D2 holds f2 . a2,(f2 . b₁,b₂) = f2 . (f2 . a2,b₁),b₂
let b2, c2 be Element of D2; :: thesis: f2 . a2,(f2 . b2,c2) = f2 . (f2 . a2,b2),c2
[(f1 . a1,(f1 . b1,c1)),(f2 . a2,(f2 . b2,c2))] = |:f1,f2:| . [a1,a2],[(f1 . b1,c1),(f2 . b2,c2)] by Th22
.= |:f1,f2:| . [a1,a2],(|:f1,f2:| . [b1,b2],[c1,c2]) by Th22
.= |:f1,f2:| . (|:f1,f2:| . [a1,a2],[b1,b2]),[c1,c2] by A4
.= |:f1,f2:| . [(f1 . a1,b1),(f2 . a2,b2)],[c1,c2] by Th22
.= [(f1 . (f1 . a1,b1),c1),(f2 . (f2 . a2,b2),c2)] by Th22 ;
hence f2 . a2,(f2 . b2,c2) = f2 . (f2 . a2,b2),c2 by ZFMISC_1:33; :: thesis: verum