let D be non empty set ; :: thesis: for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let S be non empty Subset of D; :: thesis: for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let f1, f2 be BinOp of D; :: thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let g1, g2 be BinOp of S; :: thesis: ( g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2 )
assume ( g1 = f1 || S & g2 = f2 || S & f1 is_left_distributive_wrt f2 & f1 is_right_distributive_wrt f2 ) ; :: according to BINOP_1:def 11 :: thesis: g1 is_distributive_wrt g2
hence ( g1 is_left_distributive_wrt g2 & g1 is_right_distributive_wrt g2 ) by Th3; :: according to BINOP_1:def 11 :: thesis: verum