let C be non empty AltCatStr ; :: thesis: for o being Object of C
for f being ObjectsFamily of {},C holds {} is MorphismsFamily of o,f
let o be Object of C; :: thesis: for f being ObjectsFamily of {},C holds {} is MorphismsFamily of o,f
let f be ObjectsFamily of {},C; :: thesis: {} is MorphismsFamily of o,f
reconsider A = {} as {} -defined Relation ;
A is total ;
then reconsider A = {} as ManySortedSet of {} ;
A is MorphismsFamily of o,f
proof
let i be object ; :: according to ALTCAT_5:def 2 :: thesis: ( i in {} implies ex o1 being Object of C st
( o1 = f . i & A . i is Morphism of o,o1 ) )
thus ( i in {} implies ex o1 being Object of C st
( o1 = f . i & A . i is Morphism of o,o1 ) ) ; :: thesis: verum
end;
hence {} is MorphismsFamily of o,f ; :: thesis: verum