let f be non-empty Function; :: thesis: for X, Y being set
for i, j, x, y being object
for g being Function st x in X & y in Y & i <> j & g in product f holds
g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))

let X, Y be set ; :: thesis: for i, j, x, y being object
for g being Function st x in X & y in Y & i <> j & g in product f holds
g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))

let i, j, x, y be object ; :: thesis: for g being Function st x in X & y in Y & i <> j & g in product f holds
g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))

let g be Function; :: thesis: ( x in X & y in Y & i <> j & g in product f implies g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y))) )
assume that
A1: ( x in X & y in Y ) and
A2: ( i <> j & g in product f ) ; :: thesis: g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y)))
A3: dom (g +* ((i,j) --> (x,y))) = (dom g) \/ (dom ((i,j) --> (x,y))) by FUNCT_4:def 1
.= (dom g) \/ {i,j} by FUNCT_4:62
.= (dom f) \/ {i,j} by
.= (dom f) \/ (dom ((i,j) --> (X,Y))) by FUNCT_4:62
.= dom (f +* ((i,j) --> (X,Y))) by FUNCT_4:def 1 ;
for z being object st z in dom (f +* ((i,j) --> (X,Y))) holds
(g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
proof
let z be object ; :: thesis: ( z in dom (f +* ((i,j) --> (X,Y))) implies (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z )
assume A4: z in dom (f +* ((i,j) --> (X,Y))) ; :: thesis: (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
per cases ( z in {i,j} or not z in {i,j} ) ;
suppose A5: z in {i,j} ; :: thesis: (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
then z in dom ((i,j) --> (x,y)) by FUNCT_4:62;
then A6: (g +* ((i,j) --> (x,y))) . z = ((i,j) --> (x,y)) . z by FUNCT_4:13;
z in dom ((i,j) --> (X,Y)) by ;
then A7: (f +* ((i,j) --> (X,Y))) . z = ((i,j) --> (X,Y)) . z by FUNCT_4:13;
per cases ( z = i or z = j ) by ;
suppose A8: z = i ; :: thesis: (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
then (g +* ((i,j) --> (x,y))) . z = x by ;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by ; :: thesis: verum
end;
suppose A9: z = j ; :: thesis: (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
then (g +* ((i,j) --> (x,y))) . z = y by ;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by ; :: thesis: verum
end;
end;
end;
suppose A10: not z in {i,j} ; :: thesis: (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z
then not z in dom ((i,j) --> (x,y)) by FUNCT_4:62;
then A11: (g +* ((i,j) --> (x,y))) . z = g . z by FUNCT_4:11;
not z in dom ((i,j) --> (X,Y)) by ;
then A12: (f +* ((i,j) --> (X,Y))) . z = f . z by FUNCT_4:11;
z in (dom f) \/ (dom ((i,j) --> (X,Y))) by ;
then z in (dom f) \/ {i,j} by FUNCT_4:62;
then z in dom f by ;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by ; :: thesis: verum
end;
end;
end;
hence g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y))) by ; :: thesis: verum