let F be MorphismsFamily of o,f; :: thesis: F is Function-yielding
let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom F or F . i is set )
assume i in dom F ; :: thesis: F . i is set
then ex o1 being Object of C st
( o1 = f . i & F . i is Morphism of o,o1 ) by Def2;
hence F . i is set ; :: thesis: verum