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 that
A1: g1 = f1 || S and
A2: 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 A3: 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 a9 = a, b9 = b, c9 = c as Element of D ;
A4: ( f2 . [b9,c9] = f2 . b9,c9 & f1 . [a9,b9] = f1 . a9,b9 ) ;
A5: ( f1 . [a9,c9] = f1 . a9,c9 & f1 . [a,(g2 . b,c)] = f1 . a,(g2 . b,c) ) ;
dom g2 = [:S,S:] by FUNCT_2:def 1;
then A6: ( g2 . [b,c] = f2 . [b,c] & g2 . [(g1 . a,b),(g1 . a,c)] = f2 . [(g1 . a,b),(g1 . a,c)] ) by A2, FUNCT_1:70;
A7: f2 . [(g1 . a,b),(g1 . a,c)] = f2 . (g1 . a,b),(g1 . a,c) ;
A8: dom g1 = [:S,S:] by FUNCT_2:def 1;
then A9: g1 . [a,(g2 . b,c)] = f1 . [a,(g2 . b,c)] by A1, FUNCT_1:70;
( g1 . [a,b] = f1 . [a,b] & g1 . [a,c] = f1 . [a,c] ) by A1, A8, FUNCT_1:70;
hence g1 . a,(g2 . b,c) = g2 . (g1 . a,b),(g1 . a,c) by A3, A4, A9, A5, A6, A7; :: thesis: verum

end;

assume A10: 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;
A11: f2 . [(g1 . a,c),(g1 . b,c)] = f2 . (g1 . a,c),(g1 . b,c) ;
A12: dom g1 = [:S,S:] by FUNCT_2:def 1;
then A13: g1 . [(g2 . a,b),c] = f1 . [(g2 . a,b),c] by A1, FUNCT_1:70;
dom g2 = [:S,S:] by FUNCT_2:def 1;
then A14: ( g2 . [a,b] = f2 . [a,b] & g2 . [(g1 . a,c),(g1 . b,c)] = f2 . [(g1 . a,c),(g1 . b,c)] ) by A2, FUNCT_1:70;
reconsider a9 = a, b9 = b, c9 = c as Element of D ;
A15: ( f1 . [b9,c9] = f1 . b9,c9 & f2 . [a9,b9] = f2 . a9,b9 ) ;
A16: ( f1 . [a9,c9] = f1 . a9,c9 & f1 . [(g2 . a,b),c] = f1 . (g2 . a,b),c ) ;
( g1 . [b,c] = f1 . [b,c] & g1 . [a,c] = f1 . [a,c] ) by A1, A12, FUNCT_1:70;
hence g1 . (g2 . a,b),c = g2 . (g1 . a,c),(g1 . b,c) by A10, A15, A13, A16, A14, A11; :: thesis: verum