let A, B, C, D be set ; :: thesis: for a, b being object st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))
let a, b be object ; :: 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:62;
A4: for x being object st x in dom ((a,b) --> (A,C)) holds
((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x

proof

let x be object ; :: 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:63;
((a,b) --> (A,C)) . a = A by A6, FUNCT_4:63;
hence ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x by A1, A2, A5, A6, A7, FUNCT_4:63; :: 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:81;
then A9: ((a,b) --> (A,C)) . a = C by FUNCOP_1:72;
(a,b) --> (B,D) = a .--> D by A8, FUNCT_4:81;
hence ((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . x by A2, A5, A8, A9, FUNCOP_1:72; :: thesis: verum

end;

end;

end;

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