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

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

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

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

end;

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;

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

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