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
A3: for x being object st x in dom F holds
(f +* (i,xi)) . x in F . x

proof

let x be object ; :: 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:31; :: 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:9; :: 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:32;
hence (f +* (i,xi)) . x in F . x by A2, A4, CARD_3:9; :: thesis: verum

end;

end;

end;

dom f = dom F by A2, CARD_3:9;
then dom (f +* (i,xi)) = dom F by FUNCT_7:30;
hence f +* (i,xi) in product F by A3, CARD_3:9; :: thesis: verum