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

proof

assume that
A1: f1 is_left_distributive_wrt g1 and
A2: f1 is_right_distributive_wrt g1 and
A3: f2 is_left_distributive_wrt g2 and
A4: f2 is_right_distributive_wrt g2 ; :: according to BINOP_1:def 11 :: thesis: |:f1,f2:| is_distributive_wrt |:g1,g2:|
thus ( |:f1,f2:| is_left_distributive_wrt |:g1,g2:| & |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ) by A1, A2, A3, A4, Th28, Th29; :: according to BINOP_1:def 11 :: thesis: verum

end;

assume that
A5: |:f1,f2:| is_left_distributive_wrt |:g1,g2:| and
A6: |:f1,f2:| is_right_distributive_wrt |:g1,g2:| ; :: according to BINOP_1:def 11 :: thesis: ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 )
thus ( f1 is_left_distributive_wrt g1 & f1 is_right_distributive_wrt g1 & f2 is_left_distributive_wrt g2 & f2 is_right_distributive_wrt g2 ) by A5, A6, Th28, Th29; :: according to BINOP_1:def 11 :: thesis: verum