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 ; :: 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 ;
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 ;
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 ;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by ; :: 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 ;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by ; :: 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 ;
hence (f +* ((i,j) --> (A,B))) . x c= (f +* ((i,j) --> (C,D))) . x by ; :: thesis: verum
end;
end;
end;
hence product (f +* ((i,j) --> (A,B))) c= product (f +* ((i,j) --> (C,D))) by ; :: thesis: verum
end;
end;