let i, j be object ; :: thesis: for A, B, C, D being set st A c= C & B c= D holds
product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D))
let A, B, C, D be set ; :: thesis: ( A c= C & B c= D implies product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D)) )
assume A1: ( A c= C & B c= D ) ; :: thesis: product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D))
per cases ( i <> j or i = j ) ;
suppose A2: i <> j ; :: thesis: product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product ((i,j) --> (A,B)) or x in product ((i,j) --> (C,D)) )
assume x in product ((i,j) --> (A,B)) ; :: thesis: x in product ((i,j) --> (C,D))
then consider g being Function such that
A3: ( g = x & dom g = dom ((i,j) --> (A,B)) ) and
A4: for y being object st y in dom ((i,j) --> (A,B)) holds
g . y in ((i,j) --> (A,B)) . y by CARD_3:def 5;
A5: dom ((i,j) --> (A,B)) = {i,j} by FUNCT_4:62
.= dom ((i,j) --> (C,D)) by FUNCT_4:62 ;
for y being object st y in dom ((i,j) --> (C,D)) holds
g . y in ((i,j) --> (C,D)) . y
proof
let y be object ; :: thesis: ( y in dom ((i,j) --> (C,D)) implies g . y in ((i,j) --> (C,D)) . y )
assume A6: y in dom ((i,j) --> (C,D)) ; :: thesis: g . y in ((i,j) --> (C,D)) . y
then y in {i,j} by FUNCT_4:62;
per cases then ( y = i or y = j ) by TARSKI:def 2;
suppose A7: y = i ; :: thesis: g . y in ((i,j) --> (C,D)) . y
then g . y in ((i,j) --> (A,B)) . i by A4, A5, A6;
then g . y in A by A2, FUNCT_4:63;
then g . y in C by A1;
hence g . y in ((i,j) --> (C,D)) . y by A2, A7, FUNCT_4:63; :: thesis: verum
end;
suppose A8: y = j ; :: thesis: g . y in ((i,j) --> (C,D)) . y
then g . y in ((i,j) --> (A,B)) . j by A4, A5, A6;
then g . y in B by FUNCT_4:63;
then g . y in D by A1;
hence g . y in ((i,j) --> (C,D)) . y by A8, FUNCT_4:63; :: thesis: verum
end;
end;
end;
hence x in product ((i,j) --> (C,D)) by A3, A5, CARD_3:def 5; :: thesis: verum
end;
suppose A9: i = j ; :: thesis: product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D))
then A10: (i,j) --> (A,B) = i .--> B by FUNCT_4:81
.= {i} --> B by FUNCOP_1:def 9 ;
(i,j) --> (C,D) = i .--> D by A9, FUNCT_4:81
.= {i} --> D by FUNCOP_1:def 9 ;
hence product ((i,j) --> (A,B)) c= product ((i,j) --> (C,D)) by A1, A10, Th14; :: thesis: verum
end;
end;