let o, m be set ; :: thesis: the Comp of (1Cat o,m) = {[[m,m],m]}
set A = 1Cat o,m;
thus
the Comp of (1Cat o,m) c= {[[m,m],m]}
:: according to XBOOLE_0:def 10 :: thesis: {[[m,m],m]} c= the Comp of (1Cat o,m)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the Comp of (1Cat o,m) or x in {[[m,m],m]} )
consider o' being
Object of
(1Cat o,m);
A1:
(
dom (id o') = o' &
cod (id o') = o' )
by CAT_1:44;
assume A2:
x in the
Comp of
(1Cat o,m)
;
:: thesis: x in {[[m,m],m]}
then consider x1,
x2 being
set such that A3:
x = [x1,x2]
by RELAT_1:def 1;
A4:
x1 in dom the
Comp of
(1Cat o,m)
by A2, A3, RELAT_1:def 4;
dom the
Comp of
(1Cat o,m) c= [:the carrier' of (1Cat o,m),the carrier' of (1Cat o,m):]
by RELAT_1:def 18;
then consider x11,
x12 being
set such that A5:
(
x11 in the
carrier' of
(1Cat o,m) &
x12 in the
carrier' of
(1Cat o,m) )
and A6:
x1 = [x11,x12]
by A4, ZFMISC_1:def 2;
(
x11 = id o' &
x12 = id o' )
by A5, Th4;
then
x2 = the
Comp of
(1Cat o,m) . (id o'),
(id o')
by A2, A3, A4, A6, FUNCT_1:def 4;
then
x2 = (id o') * (id o')
by A1, CAT_1:41;
then
(
x11 = m &
x12 = m &
x2 = m )
by A5, TARSKI:def 1;
hence
x in {[[m,m],m]}
by A3, A6, TARSKI:def 1;
:: thesis: verum
end;
reconsider f = m as Morphism of (1Cat o,m) by TARSKI:def 1;
consider a being Object of (1Cat o,m);
A7:
f = id a
by TARSKI:def 1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[[m,m],m]} or x in the Comp of (1Cat o,m) )
assume
x in {[[m,m],m]}
; :: thesis: x in the Comp of (1Cat o,m)
then
x = [[m,m],m]
by TARSKI:def 1;
hence
x in the Comp of (1Cat o,m)
by A7, Th5; :: thesis: verum