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

proof

defpred S₁[ set , set , set ] means |:f1,f2:| . $1,(|:g1,g2:| . $2,$3) = |:g1,g2:| . (|:f1,f2:| . $1,$2),(|:f1,f2:| . $1,$3);
assume A1: for a1, b1, c1 being Element of D1 holds f1 . a1,(g1 . b1,c1) = g1 . (f1 . a1,b1),(f1 . a1,c1) ; :: according to BINOP_1:def 18 :: thesis: ( not f2 is_left_distributive_wrt g2 or |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
assume A2: for a2, b2, c2 being Element of D2 holds f2 . a2,(g2 . b2,c2) = g2 . (f2 . a2,b2),(f2 . a2,c2) ; :: according to BINOP_1:def 18 :: thesis: |:f1,f2:| is_left_distributive_wrt |:g1,g2:|

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],(|:g1,g2:| . [b1,b2],[c1,c2]) = |:f1,f2:| . [a1,a2],[(g1 . b1,c1),(g2 . b2,c2)] by Th22
.= [(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] by Th22
.= [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(f2 . a2,(g2 . b2,c2))] by A1
.= [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))] by A2
.= |:g1,g2:| . [(f1 . a1,b1),(f2 . a2,b2)],[(f1 . a1,c1),(f2 . a2,c2)] by Th22
.= |:g1,g2:| . (|:f1,f2:| . [a1,a2],[b1,b2]),[(f1 . a1,c1),(f2 . a2,c2)] by Th22
.= |:g1,g2:| . (|:f1,f2:| . [a1,a2],[b1,b2]),(|:f1,f2:| . [a1,a2],[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 18 :: thesis: verum

end;

assume A4: for a, b, c being Element of [:D1,D2:] holds |:f1,f2:| . a,(|:g1,g2:| . b,c) = |:g1,g2:| . (|:f1,f2:| . a,b),(|:f1,f2:| . a,c) ; :: according to BINOP_1:def 18 :: thesis: ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 )

A5: now

let a1, b1, c1 be Element of D1; :: thesis: for a2, b2, c2 being Element of D2 holds [(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] = [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))]
let a2, b2, c2 be Element of D2; :: thesis: [(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] = [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))]
thus [(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] = |:f1,f2:| . [a1,a2],[(g1 . b1,c1),(g2 . b2,c2)] by Th22
.= |:f1,f2:| . [a1,a2],(|:g1,g2:| . [b1,b2],[c1,c2]) by Th22
.= |:g1,g2:| . (|:f1,f2:| . [a1,a2],[b1,b2]),(|:f1,f2:| . [a1,a2],[c1,c2]) by A4
.= |:g1,g2:| . [(f1 . a1,b1),(f2 . a2,b2)],(|:f1,f2:| . [a1,a2],[c1,c2]) by Th22
.= |:g1,g2:| . [(f1 . a1,b1),(f2 . a2,b2)],[(f1 . a1,c1),(f2 . a2,c2)] by Th22
.= [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))] by Th22 ; :: thesis: verum

end;

thus for a1, b1, c1 being Element of D1 holds f1 . a1,(g1 . b1,c1) = g1 . (f1 . a1,b1),(f1 . a1,c1) :: according to BINOP_1:def 18 :: thesis: f2 is_left_distributive_wrt g2

proof

consider a2, b2, c2 being Element of D2;
let a1, b1, c1 be Element of D1; :: thesis: f1 . a1,(g1 . b1,c1) = g1 . (f1 . a1,b1),(f1 . a1,c1)
[(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] = [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))] by A5;
hence f1 . a1,(g1 . b1,c1) = g1 . (f1 . a1,b1),(f1 . a1,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 18 :: thesis: for b₁, b₂ being Element of D2 holds f2 . a2,(g2 . b₁,b₂) = g2 . (f2 . a2,b₁),(f2 . a2,b₂)
let b2, c2 be Element of D2; :: thesis: f2 . a2,(g2 . b2,c2) = g2 . (f2 . a2,b2),(f2 . a2,c2)
[(f1 . a1,(g1 . b1,c1)),(f2 . a2,(g2 . b2,c2))] = [(g1 . (f1 . a1,b1),(f1 . a1,c1)),(g2 . (f2 . a2,b2),(f2 . a2,c2))] by A5;
hence f2 . a2,(g2 . b2,c2) = g2 . (f2 . a2,b2),(f2 . a2,c2) by ZFMISC_1:33; :: thesis: verum