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_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
let f1, g1 be BinOp of D1; :: thesis: for f2, g2 being BinOp of D2 holds
( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
let f2, g2 be BinOp of D2; :: thesis: ( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
thus ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 implies |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ) :: thesis: ( |:f1,f2:| is_right_distributive_wrt |:g1,g2:| implies ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) )

proof

defpred S₁[ set , set , set ] means |:f1,f2:| . ((|:g1,g2:| . ($2,$3)),$1) = |:g1,g2:| . ((|:f1,f2:| . ($2,$1)),(|:f1,f2:| . ($3,$1)));
assume A1: for b1, c1, a1 being Element of D1 holds f1 . ((g1 . (b1,c1)),a1) = g1 . ((f1 . (b1,a1)),(f1 . (c1,a1))) ; :: according to BINOP_1:def 19 :: thesis: ( not f2 is_right_distributive_wrt g2 or |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
assume A2: for b2, c2, a2 being Element of D2 holds f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))) ; :: according to BINOP_1:def 19 :: thesis: |:f1,f2:| is_right_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:| . ((|:g1,g2:| . ([b1,b2],[c1,c2])),[a1,a2]) = |:f1,f2:| . ([(g1 . (b1,c1)),(g2 . (b2,c2))],[a1,a2]) by Th21
.= [(f1 . ((g1 . (b1,c1)),a1)),(f2 . ((g2 . (b2,c2)),a2))] by Th21
.= [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(f2 . ((g2 . (b2,c2)),a2))] by A1
.= [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))] by A2
.= |:g1,g2:| . ([(f1 . (b1,a1)),(f2 . (b2,a2))],[(f1 . (c1,a1)),(f2 . (c2,a2))]) by Th21
.= |:g1,g2:| . ((|:f1,f2:| . ([b1,b2],[a1,a2])),[(f1 . (c1,a1)),(f2 . (c2,a2))]) by Th21
.= |:g1,g2:| . ((|:f1,f2:| . ([b1,b2],[a1,a2])),(|:f1,f2:| . ([c1,c2],[a1,a2]))) by Th21 ;
hence S₁[[a1,a2],[b1,b2],[c1,c2]] ; :: thesis: verum

end;

for a, b, c being Element of [:D1,D2:] holds S₁[a,b,c] from FILTER_1:sch 6(A3);
then for b, c, a being Element of [:D1,D2:] holds S₁[a,b,c] ;
hence |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ; :: thesis: verum

end;

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

A5: now :: thesis: for a1, b1, c1 being Element of D1
for a2, b2, c2 being Element of D2 holds [(f1 . ((g1 . (b1,c1)),a1)),(f2 . ((g2 . (b2,c2)),a2))] = [(g1 . ((f1 . (b1,a1)),(f1 . (c1,a1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))]

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

end;

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

proof

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

end;

set a1 = the Element of D1;
let b2 be Element of D2; :: according to BINOP_1:def 19 :: thesis: for b₁, b₂ being Element of D2 holds f2 . ((g2 . (b2,b₁)),b₂) = g2 . ((f2 . (b2,b₂)),(f2 . (b₁,b₂)))
let c2, a2 be Element of D2; :: thesis: f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2)))
[(f1 . ((g1 . ( the Element of D1, the Element of D1)), the Element of D1)),(f2 . ((g2 . (b2,c2)),a2))] = [(g1 . ((f1 . ( the Element of D1, the Element of D1)),(f1 . ( the Element of D1, the Element of D1)))),(g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))))] by A5;
hence f2 . ((g2 . (b2,c2)),a2) = g2 . ((f2 . (b2,a2)),(f2 . (c2,a2))) by XTUPLE_0:1; :: thesis: verum