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

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

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

end;

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