let C be non empty AltCatStr ; :: thesis: for o being Object of C
for f being ObjectsFamily of {},C holds {} is MorphismsFamily of f,o
let o be Object of C; :: thesis: for f being ObjectsFamily of {},C holds {} is MorphismsFamily of f,o
let f be ObjectsFamily of {},C; :: thesis: {} is MorphismsFamily of f,o
reconsider A = {} as {} -defined Relation ;
A is total ;
then reconsider A = {} as ManySortedSet of {} ;
A is MorphismsFamily of f,o

proof

let i be object ; :: according to ALTCAT_6:def 1 :: thesis: ( i in {} implies ex o1 being Object of C st
( o1 = f . i & A . i is Morphism of o1,o ) )
thus ( i in {} implies ex o1 being Object of C st
( o1 = f . i & A . i is Morphism of o1,o ) ) ; :: thesis: verum

end;

hence {} is MorphismsFamily of f,o ; :: thesis: verum