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))

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 )
;

end;

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

end;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

hence
x in product ((i,j) --> (C,D))
by A3, A5, CARD_3:def 5; :: thesis: verum
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;

end;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;

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;.= {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