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 3 :: 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 3 :: thesis: |:f1,f2:| is associative

A3: now :: thesis: for a1, b1, c1 being Element of D1
for a2, b2, c2 being Element of D2 holds S₁[[a1,a2],[b1,b2],[c1,c2]]

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 Th21
.= [(f1 . (a1,(f1 . (b1,c1)))),(f2 . (a2,(f2 . (b2,c2))))] by Th21
.= [(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 Th21
.= |:f1,f2:| . ((|:f1,f2:| . ([a1,a2],[b1,b2])),[c1,c2]) by Th21 ;
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 3 :: 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 3 :: 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 3 :: thesis: f2 is associative

proof

set a2 = the 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 . ( the Element of D2,(f2 . ( the Element of D2, the Element of D2))))] = |:f1,f2:| . ([a1, the Element of D2],[(f1 . (b1,c1)),(f2 . ( the Element of D2, the Element of D2))]) by Th21
.= |:f1,f2:| . ([a1, the Element of D2],(|:f1,f2:| . ([b1, the Element of D2],[c1, the Element of D2]))) by Th21
.= |:f1,f2:| . ((|:f1,f2:| . ([a1, the Element of D2],[b1, the Element of D2])),[c1, the Element of D2]) by A4
.= |:f1,f2:| . ([(f1 . (a1,b1)),(f2 . ( the Element of D2, the Element of D2))],[c1, the Element of D2]) by Th21
.= [(f1 . ((f1 . (a1,b1)),c1)),(f2 . ((f2 . ( the Element of D2, the Element of D2)), the Element of D2))] by Th21 ;
hence f1 . (a1,(f1 . (b1,c1))) = f1 . ((f1 . (a1,b1)),c1) by XTUPLE_0:1; :: thesis: verum

end;

set a1 = the Element of D1;
let a2 be Element of D2; :: according to BINOP_1:def 3 :: 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 . ( the Element of D1,(f1 . ( the Element of D1, the Element of D1)))),(f2 . (a2,(f2 . (b2,c2))))] = |:f1,f2:| . ([ the Element of D1,a2],[(f1 . ( the Element of D1, the Element of D1)),(f2 . (b2,c2))]) by Th21
.= |:f1,f2:| . ([ the Element of D1,a2],(|:f1,f2:| . ([ the Element of D1,b2],[ the Element of D1,c2]))) by Th21
.= |:f1,f2:| . ((|:f1,f2:| . ([ the Element of D1,a2],[ the Element of D1,b2])),[ the Element of D1,c2]) by A4
.= |:f1,f2:| . ([(f1 . ( the Element of D1, the Element of D1)),(f2 . (a2,b2))],[ the Element of D1,c2]) by Th21
.= [(f1 . ((f1 . ( the Element of D1, the Element of D1)), the Element of D1)),(f2 . ((f2 . (a2,b2)),c2))] by Th21 ;
hence f2 . (a2,(f2 . (b2,c2))) = f2 . ((f2 . (a2,b2)),c2) by XTUPLE_0:1; :: thesis: verum