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 CARD_3:def 16;
i in dom f by A2, A3, CARD_3:9;
then (f +* (i,xi)) . i = xi by FUNCT_7:31;
then (f +* (i,xi)) . i in {xi} by TARSKI:def 1;
then (proj (F,i)) . (f +* (i,xi)) in {xi} by A4, CARD_3:def 16;
hence f +* (i,xi) in (proj (F,i)) " {xi} by A4, FUNCT_1:def 7; :: thesis: verum