let F be ManySortedSet of I; :: thesis: ( F is MorphismsFamily of o,f iff for i being Element of I holds F . i is Morphism of o,(f . i) )

hereby :: thesis: ( ( for i being Element of I holds F . i is Morphism of o,(f . i) ) implies F is MorphismsFamily of o,f )

assume A1: F is MorphismsFamily of o,f ; :: thesis: for i being Element of I holds F . i is Morphism of o,(f . i)
let i be Element of I; :: thesis: F . i is Morphism of o,(f . i)
ex o1 being Object of C st
( o1 = f . i & F . i is Morphism of o,o1 ) by A1, Def2;
hence F . i is Morphism of o,(f . i) ; :: thesis: verum

end;

assume A2: for i being Element of I holds F . i is Morphism of o,(f . i) ; :: thesis: F is MorphismsFamily of o,f
let i be object ; :: according to ALTCAT_5:def 2 :: thesis: ( i in I implies ex o1 being Object of C st
( o1 = f . i & F . i is Morphism of o,o1 ) )
assume i in I ; :: thesis: ex o1 being Object of C st
( o1 = f . i & F . i is Morphism of o,o1 )
then reconsider j = i as Element of I ;
take f . j ; :: thesis: ( f . j = f . i & F . i is Morphism of o,(f . j) )
thus ( f . j = f . i & F . i is Morphism of o,(f . j) ) by A2; :: thesis: verum