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 A1: ( A c= B & 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;
A2: ( dom (a,b --> A,C) = {a,b} & dom (a,b --> B,D) = {a,b} ) by FUNCT_4:65;
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 A3: ( x = a or x = b ) by A2, TARSKI:def 2;

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

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

then ( (a,b --> A,C) . a = A & (a,b --> A,C) . b = C & (a,b --> B,D) . a = B & (a,b --> B,D) . b = D ) by FUNCT_4:66;
hence (a,b --> A,C) . x c= (a,b --> B,D) . x by A1, A3; :: thesis: verum

end;

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

then ( a,b --> A,C = a .--> C & a,b --> B,D = a .--> D ) by FUNCT_4:86;
then ( (a,b --> A,C) . a = C & (a,b --> A,C) . b = C & (a,b --> B,D) . b = D & (a,b --> B,D) . b = D ) by A4, FUNCOP_1:87;
hence (a,b --> A,C) . x c= (a,b --> B,D) . x by A1, A3, A4; :: thesis: verum

end;

end;

end;

hence product (a,b --> A,C) c= product (a,b --> B,D) by A2, CARD_3:38; :: thesis: verum