let F, f be Function; :: thesis: for i, xi being set st xi in F . i & i in dom F & f in product F holds
f +* i,xi in (proj F,i) " {xi}
let i, xi be set ; :: thesis: ( xi in F . i & i in dom F & f in product F implies f +* i,xi in (proj F,i) " {xi} )
assume that
A1: xi in F . i and
A2: i in dom F and
A3: f in product F ; :: thesis: f +* i,xi in (proj F,i) " {xi}
f +* i,xi in product F by A1, A3, Th2;
then A4: f +* i,xi in dom (proj F,i) by PRALG_3:def 2;
i in dom f by A2, A3, CARD_3:18;
then (f +* i,xi) . i = xi by FUNCT_7:33;
then (f +* i,xi) . i in {xi} by TARSKI:def 1;
then (proj F,i) . (f +* i,xi) in {xi} by A4, PRALG_3:def 2;
hence f +* i,xi in (proj F,i) " {xi} by A4, FUNCT_1:def 13; :: thesis: verum