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 holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_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 holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_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 holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let g1, g2 be BinOp of S; :: thesis: ( g1 = f1 || S & g2 = f2 || S implies ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) )
assume A1: ( g1 = f1 || S & g2 = f2 || S ) ; :: thesis: ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
thus ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) :: thesis: ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 )

proof

assume A2: for a, b, c being Element of D holds f1 . a,(f2 . b,c) = f2 . (f1 . a,b),(f1 . a,c) ; :: according to BINOP_1:def 18 :: thesis: g1 is_left_distributive_wrt g2
let a, b, c be Element of S; :: according to BINOP_1:def 18 :: thesis: g1 . a,(g2 . b,c) = g2 . (g1 . a,b),(g1 . a,c)
set ab = g1 . a,b;
set ac = g1 . a,c;
set bc = g2 . b,c;
reconsider a' = a, b' = b, c' = c as Element of D ;
( [a,b] in [:S,S:] & [a,c] in [:S,S:] & [b,c] in [:S,S:] & [a,(g2 . b,c)] in [:S,S:] & [(g1 . a,b),(g1 . a,c)] in [:S,S:] & dom g1 = [:S,S:] & dom g2 = [:S,S:] ) by FUNCT_2:def 1;
then ( g2 . b,c = g2 . [b,c] & g2 . [b,c] = f2 . [b,c] & f2 . [b',c'] = f2 . b',c' & g1 . a,b = g1 . [a,b] & g1 . [a,b] = f1 . [a,b] & f1 . [a',b'] = f1 . a',b' & g1 . a,c = g1 . [a,c] & g1 . [a,c] = f1 . [a,c] & f1 . [a',c'] = f1 . a',c' & g1 . a,(g2 . b,c) = g1 . [a,(g2 . b,c)] & g1 . [a,(g2 . b,c)] = f1 . [a,(g2 . b,c)] & f1 . [a,(g2 . b,c)] = f1 . a,(g2 . b,c) & g2 . (g1 . a,b),(g1 . a,c) = g2 . [(g1 . a,b),(g1 . a,c)] & g2 . [(g1 . a,b),(g1 . a,c)] = f2 . [(g1 . a,b),(g1 . a,c)] & f2 . [(g1 . a,b),(g1 . a,c)] = f2 . (g1 . a,b),(g1 . a,c) ) by A1, FUNCT_1:70;
hence g1 . a,(g2 . b,c) = g2 . (g1 . a,b),(g1 . a,c) by A2; :: thesis: verum

end;

assume A3: for a, b, c being Element of D holds f1 . (f2 . a,b),c = f2 . (f1 . a,c),(f1 . b,c) ; :: according to BINOP_1:def 19 :: thesis: g1 is_right_distributive_wrt g2
let a, b, c be Element of S; :: according to BINOP_1:def 19 :: thesis: g1 . (g2 . a,b),c = g2 . (g1 . a,c),(g1 . b,c)
set ab = g2 . a,b;
set ac = g1 . a,c;
set bc = g1 . b,c;
reconsider a' = a, b' = b, c' = c as Element of D ;
( [a,b] in [:S,S:] & [a,c] in [:S,S:] & [b,c] in [:S,S:] & [a,(g1 . b,c)] in [:S,S:] & [(g2 . a,b),(g1 . a,c)] in [:S,S:] & dom g1 = [:S,S:] & dom g2 = [:S,S:] ) by FUNCT_2:def 1;
then ( g1 . b,c = g1 . [b,c] & g1 . [b,c] = f1 . [b,c] & f1 . [b',c'] = f1 . b',c' & g2 . a,b = g2 . [a,b] & g2 . [a,b] = f2 . [a,b] & f2 . [a',b'] = f2 . a',b' & g1 . a,c = g1 . [a,c] & g1 . [a,c] = f1 . [a,c] & f1 . [a',c'] = f1 . a',c' & g1 . (g2 . a,b),c = g1 . [(g2 . a,b),c] & g1 . [(g2 . a,b),c] = f1 . [(g2 . a,b),c] & f1 . [(g2 . a,b),c] = f1 . (g2 . a,b),c & g2 . (g1 . a,c),(g1 . b,c) = g2 . [(g1 . a,c),(g1 . b,c)] & g2 . [(g1 . a,c),(g1 . b,c)] = f2 . [(g1 . a,c),(g1 . b,c)] & f2 . [(g1 . a,c),(g1 . b,c)] = f2 . (g1 . a,c),(g1 . b,c) ) by A1, FUNCT_1:70;
hence g1 . (g2 . a,b),c = g2 . (g1 . a,c),(g1 . b,c) by A3; :: thesis: verum