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 :: 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],(|:g1,g2:| . ([b1,b2],[c1,c2]))) = |:f1,f2:| . ([a1,a2],[(g1 . (b1,c1)),(g2 . (b2,c2))]) by Th21
.= [(f1 . (a1,(g1 . (b1,c1)))),(f2 . (a2,(g2 . (b2,c2))))] by Th21
.= [(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 Th21
.= |:g1,g2:| . ((|:f1,f2:| . ([a1,a2],[b1,b2])),[(f1 . (a1,c1)),(f2 . (a2,c2))]) by Th21
.= |:g1,g2:| . ((|:f1,f2:| . ([a1,a2],[b1,b2])),(|:f1,f2:| . ([a1,a2],[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 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 :: thesis: for a1, b1, c1 being Element of D1
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 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 Th21
.= |:f1,f2:| . ([a1,a2],(|:g1,g2:| . ([b1,b2],[c1,c2]))) by Th21
.= |: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 Th21
.= |:g1,g2:| . ([(f1 . (a1,b1)),(f2 . (a2,b2))],[(f1 . (a1,c1)),(f2 . (a2,c2))]) by Th21
.= [(g1 . ((f1 . (a1,b1)),(f1 . (a1,c1)))),(g2 . ((f2 . (a2,b2)),(f2 . (a2,c2))))] by Th21 ; :: 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

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