let f be Function; :: thesis: for A, B, C, D being set
for i, j being object st A c= C & B c= D holds
product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))
let A, B, C, D be set ; :: thesis: for i, j being object st A c= C & B c= D holds
product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))
let i, j be object ; :: thesis: ( A c= C & B c= D implies product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D))) )
assume A1: ( A c= C & B c= D ) ; :: thesis: product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))

then ( (i,j) --> (A,B) = i .--> B & (i,j) --> (C,D) = i .--> D ) by FUNCT_4:81;
hence product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D))) by A1, Th27; :: thesis: verum

end;

suppose A2: i <> j ; :: thesis: product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D)))

dom (f +* ((i,j) --> (A,B))) = (dom f) \/ (dom ((i,j) --> (A,B))) by FUNCT_4:def 1
.= (dom f) \/ {i,j} by FUNCT_4:62 ;
then A3: dom (f +* ((i,j) --> (A,B))) = (dom f) \/ (dom ((i,j) --> (C,D))) by FUNCT_4:62
.= dom (f +* ((i,j) --> (C,D))) by FUNCT_4:def 1 ;
for x being object st x in dom (f +* ((i,j) --> (A,B))) holds
(f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

proof

let x be object ; :: thesis: ( x in dom (f +* ((i,j) --> (A,B))) implies (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x )
assume x in dom (f +* ((i,j) --> (A,B))) ; :: thesis: (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

per cases ( x in {i,j} or not x in {i,j} ) ;

suppose A4: x in {i,j} ; :: thesis: (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

then x in dom ((i,j) --> (A,B)) by FUNCT_4:62;
then A5: (f +* ((i,j) --> (A,B))) . x = ((i,j) --> (A,B)) . x by FUNCT_4:13;
x in dom ((i,j) --> (C,D)) by A4, FUNCT_4:62;
then A6: (f +* ((i,j) --> (C,D))) . x = ((i,j) --> (C,D)) . x by FUNCT_4:13;

per cases ( x = i or x = j ) by A4, TARSKI:def 2;

suppose A7: x = i ; :: thesis: (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

then (f +* ((i,j) --> (A,B))) . x = A by A2, A5, FUNCT_4:63;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by A1, A2, A6, A7, FUNCT_4:63; :: thesis: verum

end;

suppose A9: x = j ; :: thesis: (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

then (f +* ((i,j) --> (A,B))) . x = B by A5, FUNCT_4:63;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by A1, A6, A9, FUNCT_4:63; :: thesis: verum

end;

end;

end;

suppose A11: not x in {i,j} ; :: thesis: (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x

then not x in dom ((i,j) --> (A,B)) by FUNCT_4:62;
then A12: (f +* ((i,j) --> (A,B))) . x = f . x by FUNCT_4:11;
not x in dom ((i,j) --> (C,D)) by A11, FUNCT_4:62;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by A12, FUNCT_4:11; :: thesis: verum

end;

end;

end;

hence product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D))) by A3, CARD_3:27; :: thesis: verum

end;

end;