let A, B, C, D be set ; 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 ; ( 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
; 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 ;
( 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))
;
((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
;
((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . xA7:
((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;
verum end; suppose A8:
a = b
;
((a,b) --> (A,C)) . x c= ((a,b) --> (B,D)) . xthen
(
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;
verum 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; verum