let o, m be set ; c1Cat* (o,m) is Category-like
set C = c1Cat* (o,m);
set CP = the Comp of (c1Cat* (o,m));
set CD = the Source of (c1Cat* (o,m));
set CC = the Target of (c1Cat* (o,m));
thus
for f, g being Morphism of (c1Cat* (o,m)) holds
( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f )
CAT_1:def 6 verumproof
let f,
g be
Morphism of
(c1Cat* (o,m));
( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f )
A1:
dom the
Comp of
(c1Cat* (o,m)) = {[m,m]}
by FUNCOP_1:13;
A2:
(
f = m &
g = m )
by TARSKI:def 1;
thus
(
[g,f] in dom the
Comp of
(c1Cat* (o,m)) implies
dom g = cod f )
by ZFMISC_1:def 10;
( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) )
thus
(
dom g = cod f implies
[g,f] in dom the
Comp of
(c1Cat* (o,m)) )
by A1, A2, TARSKI:def 1;
verum
end;