let F be Function; :: thesis: for i being set st i in dom F holds
(proj F,i) " (F . i) = product F
let i be set ; :: thesis: ( i in dom F implies (proj F,i) " (F . i) = product F )
assume A1: i in dom F ; :: thesis: (proj F,i) " (F . i) = product F
dom (proj F,i) = product F by CARD_3:def 17;
hence (proj F,i) " (F . i) c= product F by RELAT_1:167; :: according to XBOOLE_0:def 10 :: thesis: product F c= (proj F,i) " (F . i)
let f9 be set ; :: according to TARSKI:def 3 :: thesis: ( not f9 in product F or f9 in (proj F,i) " (F . i) )
assume A2: f9 in product F ; :: thesis: f9 in (proj F,i) " (F . i)
then consider f being Function such that
A3: f9 = f and
dom f = dom F and
A4: for x being set st x in dom F holds
f . x in F . x by CARD_3:def 5;
A5: f in dom (proj F,i) by A2, A3, CARD_3:def 17;
f . i in F . i by A1, A4;
then (proj F,i) . f in F . i by A5, CARD_3:def 17;
hence f9 in (proj F,i) " (F . i) by A3, A5, FUNCT_1:def 13; :: thesis: verum