let F be MorphismsFamily of f,o; :: thesis: F is Function-yielding
let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in proj1 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 o1,o ) by Def1;
hence F . i is set ; :: thesis: verum