let F, f be Function; :: thesis: for i, xi being set st xi in F . i & f in product F holds
f +* i,xi in product F
let i, xi be set ; :: thesis: ( xi in F . i & f in product F implies f +* i,xi in product F )
assume A1: xi in F . i ; :: thesis: ( not f in product F or f +* i,xi in product F )
assume A2: f in product F ; :: thesis: f +* i,xi in product F
then ( dom f = dom F & ( for x being set st x in dom F holds
f . x in F . x ) ) by CARD_3:18;
then A3: dom (f +* i,xi) = dom F by FUNCT_7:32;
for x being set st x in dom F holds
(f +* i,xi) . x in F . x

proof

let x be set ; :: thesis: ( x in dom F implies (f +* i,xi) . x in F . x )
assume A4: x in dom F ; :: thesis: (f +* i,xi) . x in F . x

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

suppose A5: i = x ; :: thesis: (f +* i,xi) . x in F . x

thus (f +* i,xi) . x in F . x :: thesis: verum

proof

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: (f +* i,xi) . x in F . x

hence (f +* i,xi) . x in F . x by A1, A5, FUNCT_7:33; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: (f +* i,xi) . x in F . x

then f +* i,xi = f by FUNCT_7:def 3;
hence (f +* i,xi) . x in F . x by A2, A4, CARD_3:18; :: thesis: verum

end;

end;

end;

end;

suppose i <> x ; :: thesis: (f +* i,xi) . x in F . x

then (f +* i,xi) . x = f . x by FUNCT_7:34;
hence (f +* i,xi) . x in F . x by A2, A4, CARD_3:18; :: thesis: verum

end;

end;

end;

hence f +* i,xi in product F by A3, CARD_3:18; :: thesis: verum