let A, B, C, D, a, b be set ; :: thesis: ( A c= B & C c= D implies product (a,b --> A,C) c= product (a,b --> B,D) )
assume that
A1: A c= B and
A2: C c= D ; :: thesis: product (a,b --> A,C) c= product (a,b --> B,D)
set f = a,b --> A,C;
set g = a,b --> B,D;
A3: dom (a,b --> A,C) = {a,b} by FUNCT_4:65;
A4: for x being set st x in dom (a,b --> A,C) holds
(a,b --> A,C) . x c= (a,b --> B,D) . x

proof

let x be set ; :: thesis: ( x in dom (a,b --> A,C) implies (a,b --> A,C) . x c= (a,b --> B,D) . x )
assume x in dom (a,b --> A,C) ; :: thesis: (a,b --> A,C) . x c= (a,b --> B,D) . x
then A5: ( x = a or x = b ) by A3, TARSKI:def 2;

per cases ( a <> b or a = b ) ;

suppose A6: a <> b ; :: thesis: (a,b --> A,C) . x c= (a,b --> B,D) . x

A7: (a,b --> A,C) . b = C by FUNCT_4:66;
(a,b --> A,C) . a = A by A6, FUNCT_4:66;
hence (a,b --> A,C) . x c= (a,b --> B,D) . x by A1, A2, A5, A6, A7, FUNCT_4:66; :: thesis: verum

end;

suppose A8: a = b ; :: thesis: (a,b --> A,C) . x c= (a,b --> B,D) . x

then a,b --> A,C = a .--> C by FUNCT_4:86;
then A9: (a,b --> A,C) . a = C by FUNCOP_1:87;
a,b --> B,D = a .--> D by A8, FUNCT_4:86;
hence (a,b --> A,C) . x c= (a,b --> B,D) . x by A2, A5, A8, A9, FUNCOP_1:87; :: thesis: verum

end;

end;

end;

dom (a,b --> B,D) = {a,b} by FUNCT_4:65;
hence product (a,b --> A,C) c= product (a,b --> B,D) by A4, CARD_3:38, FUNCT_4:65; :: thesis: verum