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

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 Th22
.= [(f1 . (g1 . b1,c1),a1),(f2 . (g2 . b2,c2),a2)] by Th22
.= [(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 Th22
.= |:g1,g2:| . (|:f1,f2:| . [b1,b2],[a1,a2]),[(f1 . c1,a1),(f2 . c2,a2)] by Th22
.= |:g1,g2:| . (|:f1,f2:| . [b1,b2],[a1,a2]),(|:f1,f2:| . [c1,c2],[a1,a2]) by Th22 ;
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:| by BINOP_1:def 19; :: 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

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

consider a2, b2, c2 being 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 . b2,c2),a2)] = [(g1 . (f1 . b1,a1),(f1 . c1,a1)),(g2 . (f2 . b2,a2),(f2 . c2,a2))] by A5;
hence f1 . (g1 . b1,c1),a1 = g1 . (f1 . b1,a1),(f1 . c1,a1) by ZFMISC_1:33; :: thesis: verum

end;

consider a1, b1, c1 being 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 . b1,c1),a1),(f2 . (g2 . b2,c2),a2)] = [(g1 . (f1 . b1,a1),(f1 . c1,a1)),(g2 . (f2 . b2,a2),(f2 . c2,a2))] by A5;
hence f2 . (g2 . b2,c2),a2 = g2 . (f2 . b2,a2),(f2 . c2,a2) by ZFMISC_1:33; :: thesis: verum