let F, f be Function; 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 ; ( 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
; 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; verum