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 A2, CARD_3:9
.= (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 A5, FUNCT_4:62;
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 A5, TARSKI:def 2;

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 A2, A6, FUNCT_4:63;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by A1, A2, A7, A8, FUNCT_4:63; :: 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 A6, FUNCT_4:63;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by A1, A7, A9, FUNCT_4:63; :: 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 A10, FUNCT_4:62;
then A12: (f +* ((i,j) --> (X,Y))) . z = f . z by FUNCT_4:11;
z in (dom f) \/ (dom ((i,j) --> (X,Y))) by A4, FUNCT_4:def 1;
then z in (dom f) \/ {i,j} by FUNCT_4:62;
then z in dom f by A10, XBOOLE_0:def 3;
hence (g +* ((i,j) --> (x,y))) . z in (f +* ((i,j) --> (X,Y))) . z by A2, A11, A12, CARD_3:9; :: thesis: verum

end;

end;

end;

hence g +* ((i,j) --> (x,y)) in product (f +* ((i,j) --> (X,Y))) by A3, CARD_3:9; :: thesis: verum