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:47;
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:47;
( g1 . [a,b] = f1 . [a,b] & g1 . [a,c] = f1 . [a,c] ) by A1, A8, FUNCT_1:47;
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:47;
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:47;
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:47;
hence g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c))) by A10, A15, A13, A16, A14, A11; :: thesis: verum