let o, m be set ; for a, b being Object of (c1Cat* (o,m))
for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b
let a, b be Object of (c1Cat* (o,m)); for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b
let f be Morphism of (c1Cat* (o,m)); f is Morphism of a,b
f in Hom (a,b)
by Th47;
hence
f is Morphism of a,b
by CAT_1:def 5; verum