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

(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