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 16;
hence (proj (F,i)) " (F . i) c= product F by RELAT_1:132; :: according to XBOOLE_0:def 10 :: thesis: product F c= (proj (F,i)) " (F . i)
let f9 be object ; :: 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 object 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 16;
f . i in F . i by A1, A4;
then (proj (F,i)) . f in F . i by A5, CARD_3:def 16;
hence f9 in (proj (F,i)) " (F . i) by A3, A5, FUNCT_1:def 7; :: thesis: verum