reconsider O = commaObjs (F,G), M = commaMorphs (F,G) as non empty set ;
defpred S1[ Element of commaObjs (F,G), set ] means $2 = [[$1,$1],[(id ($1 `11)),(id ($1 `12))]];
deffunc H3( Element of commaMorphs (F,G)) -> Element of commaObjs (F,G) = $1 `12 ;
deffunc H4( Element of commaMorphs (F,G)) -> Element of commaObjs (F,G) = $1 `11 ;
consider D9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that
A2:
for k being Element of commaMorphs (F,G) holds D9 . k = H4(k)
from FUNCT_2:sch 4();
set I = the Function of (commaObjs (F,G)),(commaMorphs (F,G));
reconsider I = the Function of (commaObjs (F,G)),(commaMorphs (F,G)) as Function of O,M ;
reconsider a9 = commaComp (F,G) as PartFunc of [:M,M:],M ;
consider C9 being Function of (commaMorphs (F,G)),(commaObjs (F,G)) such that
A3:
for k being Element of commaMorphs (F,G) holds C9 . k = H3(k)
from FUNCT_2:sch 4();
reconsider D9 = D9, C9 = C9 as Function of M,O ;
set FG = CatStr(# O,M,D9,C9,a9 #);
A4:
dom the Comp of CatStr(# O,M,D9,C9,a9 #) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 }
by Def4;
A5:
for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #)
for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #);
for k1, k2 being Element of commaMorphs (F,G) st f = k1 & g = k2 & dom g = cod f holds
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]let k1,
k2 be
Element of
commaMorphs (
F,
G);
( f = k1 & g = k2 & dom g = cod f implies g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] )
assume that A6:
(
f = k1 &
g = k2 )
and A7:
dom g = cod f
;
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
A8:
(
dom g = k2 `11 &
cod f = k1 `12 )
by A2, A3, A6;
then A9:
[k2,k1] in dom a9
by A4, A7;
then A10:
a9 . (
k2,
k1)
= k2 * k1
by Def4;
g (*) f = a9 . (
g,
f)
by A6, A9, CAT_1:def 1;
hence
g (*) f = [[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]]
by A1, A6, A7, A8, A10, Def3;
verum
end;
A11:
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds Hom (b,b) <> {}
proof
let b be
Element of
CatStr(#
O,
M,
D9,
C9,
a9 #);
Hom (b,b) <> {}
reconsider o =
b as
Element of
commaObjs (
F,
G) ;
set i =
[[o,o],[(id (o `11)),(id (o `12))]];
reconsider g =
id (o `11) as
Morphism of
C ;
reconsider h =
id (o `12) as
Morphism of
D ;
A12:
dom g = o `11
by CAT_1:58;
A13:
cod g = o `11
by CAT_1:58;
A14:
dom h = o `12
by CAT_1:58;
A15:
cod h = o `12
by CAT_1:58;
o in commaObjs (
F,
G)
;
then
o in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) }
by A1, Def1;
then consider c being
Object of
C,
d being
Object of
D,
f being
Morphism of
E such that A16:
o = [[c,d],f]
and A17:
f in Hom (
(F . c),
(G . d))
;
A18:
F . g = id (F . (o `11))
by CAT_1:71;
A19:
G . h = id (G . (o `12))
by CAT_1:71;
A20:
[[c,d],f] `2 = f
;
A21:
c = o `11
by A16, MCART_1:85;
A22:
d = o `12
by A16, MCART_1:85;
A23:
cod (o `2) =
cod f
by A20, A16
.=
G . d
by A17, CAT_1:1
.=
G . (o `12)
by A22
;
dom (o `2) =
F . c
by A16, A17, CAT_1:1, A20
.=
F . (o `11)
by A21
;
then A24:
(o `2) (*) (F . g) =
o `2
by A18, CAT_1:22
.=
(G . h) (*) (o `2)
by A19, A23, CAT_1:21
;
[[o,o],[(id (o `11)),(id (o `12))]] in { [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) ) }
by A12, A13, A14, A15, A24;
then
[[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (
F,
G)
by Def2, A1;
then reconsider i =
[[o,o],[(id (o `11)),(id (o `12))]] as
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #) ;
A25:
cod i =
C9 . i
.=
[[o,o],[g,h]] `12
by A3
.=
b
by MCART_1:85
;
dom i =
D9 . i
.=
[[o,o],[g,h]] `11
by A2
.=
b
by MCART_1:85
;
then
i in Hom (
b,
b)
by A25;
hence
Hom (
b,
b)
<> {}
;
verum
end;
A26:
for a being Element of CatStr(# O,M,D9,C9,a9 #) ex i being Morphism of a,a st
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proof
let a be
Element of
CatStr(#
O,
M,
D9,
C9,
a9 #);
ex i being Morphism of a,a st
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
reconsider o =
a as
Element of
commaObjs (
F,
G) ;
set i =
[[o,o],[(id (o `11)),(id (o `12))]];
reconsider g =
id (o `11) as
Morphism of
C ;
reconsider h =
id (o `12) as
Morphism of
D ;
A27:
dom g = o `11
by CAT_1:58;
A28:
cod g = o `11
by CAT_1:58;
A29:
dom h = o `12
by CAT_1:58;
A30:
cod h = o `12
by CAT_1:58;
o in commaObjs (
F,
G)
;
then
o in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom ((F . c),(G . d)) }
by A1, Def1;
then consider c being
Object of
C,
d being
Object of
D,
f being
Morphism of
E such that A31:
o = [[c,d],f]
and A32:
f in Hom (
(F . c),
(G . d))
;
A33:
F . g = id (F . (o `11))
by CAT_1:71;
A34:
G . h = id (G . (o `12))
by CAT_1:71;
A35:
[[c,d],f] `2 = f
;
A36:
c = o `11
by A31, MCART_1:85;
A37:
d = o `12
by A31, MCART_1:85;
A38:
cod (o `2) =
cod f
by A35, A31
.=
G . d
by A32, CAT_1:1
.=
G . (o `12)
by A37
;
dom (o `2) =
F . c
by A31, A32, CAT_1:1, A35
.=
F . (o `11)
by A36
;
then A39:
(o `2) (*) (F . g) =
o `2
by A33, CAT_1:22
.=
(G . h) (*) (o `2)
by A34, A38, CAT_1:21
;
[[o,o],[(id (o `11)),(id (o `12))]] in { [[o1,o2],[gg,hh]] where gg is Morphism of C, hh is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom gg = o1 `11 & cod gg = o2 `11 & dom hh = o1 `12 & cod hh = o2 `12 & (o2 `2) (*) (F . gg) = (G . hh) (*) (o1 `2) ) }
by A27, A28, A29, A30, A39;
then
[[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (
F,
G)
by Def2, A1;
then reconsider i =
[[o,o],[(id (o `11)),(id (o `12))]] as
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #) ;
A40:
cod i =
C9 . i
.=
[[o,o],[g,h]] `12
by A3
.=
a
by MCART_1:85
;
dom i =
D9 . i
.=
[[o,o],[g,h]] `11
by A2
.=
a
by MCART_1:85
;
then
i in Hom (
a,
a)
by A40;
then reconsider i =
i as
Morphism of
a,
a by CAT_1:def 5;
take
i
;
for b being Element of CatStr(# O,M,D9,C9,a9 #) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be
Element of
CatStr(#
O,
M,
D9,
C9,
a9 #);
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) i = g )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )proof
assume A41:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) i = g
let g be
Morphism of
a,
b;
g (*) i = g
reconsider gg =
g as
Element of
commaMorphs (
F,
G) ;
reconsider ii =
i as
Element of
commaMorphs (
F,
G) ;
A42:
commaMorphs (
F,
G)
= { [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) }
by A1, Def2;
gg in commaMorphs (
F,
G)
;
then consider g1 being
Morphism of
C,
h1 being
Morphism of
D,
o1,
o2 being
Element of
commaObjs (
F,
G)
such that A43:
gg = [[o1,o2],[g1,h1]]
and A44:
dom g1 = o1 `11
and
cod g1 = o2 `11
and A45:
dom h1 = o1 `12
and
(
cod h1 = o2 `12 &
(o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) )
by A42;
A46:
dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 }
by Def4;
A47:
ii `21 =
[[o,o],[(id (o `11)),(id (o `12))]] `21
.=
id (o `11)
by MCART_1:85
;
A48:
ii `22 =
[[o,o],[(id (o `11)),(id (o `12))]] `22
.=
id (o `12)
by MCART_1:85
;
A49:
o1 =
[[o1,o2],[g1,h1]] `11
by MCART_1:85
.=
gg `11
by A43
;
A50:
o2 =
[[o1,o2],[g1,h1]] `12
by MCART_1:85
.=
gg `12
by A43
;
A51:
g1 =
[[o1,o2],[g1,h1]] `21
by MCART_1:85
.=
gg `21
by A43
;
A52:
h1 =
[[o1,o2],[g1,h1]] `22
by MCART_1:85
.=
gg `22
by A43
;
A53:
dom g = a
by A41, CAT_1:5;
A54:
dom g =
gg `11
by A2
.=
[[o1,o2],[g1,h1]] `11
by A43
.=
o1
by MCART_1:85
;
A55:
o1 =
a
by A41, CAT_1:5, A54
.=
[[c,d],f]
by A31
;
A56:
dom (gg `21) =
dom ([[o1,o2],[g1,h1]] `21)
by A43
.=
dom g1
by MCART_1:85
.=
o1 `11
by A44
.=
[[c,d],f] `11
by A55
.=
o `11
by A31
;
A57:
dom (gg `22) =
dom ([[o1,o2],[g1,h1]] `22)
by A43
.=
dom h1
by MCART_1:85
.=
o1 `12
by A45
.=
[[c,d],f] `12
by A55
.=
o `12
by A31
;
A58:
ii `11 =
[[o,o],[(id (o `11)),(id (o `12))]] `11
.=
dom g
by A53, MCART_1:85
.=
D9 . gg
.=
gg `11
by A2
;
A59:
ii `11 =
o
by MCART_1:85
.=
ii `12
by MCART_1:85
;
then
gg `11 = ii `12
by A58;
then A60:
[gg,ii] in dom (commaComp (F,G))
by A46;
hence g (*) i =
(commaComp (F,G)) . (
g,
i)
by CAT_1:def 1
.=
gg * ii
by A60, Def4
.=
[[(gg `11),(gg `12)],[((gg `21) (*) (id (o `11))),((gg `22) (*) (ii `22))]]
by A1, A59, Def3, A58, A47
.=
[[(gg `11),(gg `12)],[(gg `21),((gg `22) (*) (ii `22))]]
by A56, CAT_1:22
.=
[[(gg `11),(gg `12)],[(gg `21),(gg `22)]]
by CAT_1:22, A48, A57
.=
g
by A49, A50, A51, A52, A43
;
verum
end;
thus
(
Hom (
b,
a)
<> {} implies for
f being
Morphism of
b,
a holds
i (*) f = f )
verumproof
assume A61:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds i (*) f = f
let g be
Morphism of
b,
a;
i (*) g = g
reconsider gg =
g as
Element of
commaMorphs (
F,
G) ;
reconsider ii =
i as
Element of
commaMorphs (
F,
G) ;
A62:
commaMorphs (
F,
G)
= { [[o1,o2],[g1,h1]] where g1 is Morphism of C, h1 is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g1 = o1 `11 & cod g1 = o2 `11 & dom h1 = o1 `12 & cod h1 = o2 `12 & (o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) ) }
by A1, Def2;
gg in commaMorphs (
F,
G)
;
then consider g1 being
Morphism of
C,
h1 being
Morphism of
D,
o1,
o2 being
Element of
commaObjs (
F,
G)
such that A63:
gg = [[o1,o2],[g1,h1]]
and
dom g1 = o1 `11
and A64:
cod g1 = o2 `11
and
dom h1 = o1 `12
and A65:
cod h1 = o2 `12
and
(o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2)
by A62;
A66:
dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 }
by Def4;
A67:
ii `21 =
[[o,o],[(id (o `11)),(id (o `12))]] `21
.=
id (o `11)
by MCART_1:85
;
A68:
ii `22 =
[[o,o],[(id (o `11)),(id (o `12))]] `22
.=
id (o `12)
by MCART_1:85
;
A69:
o1 =
[[o1,o2],[g1,h1]] `11
by MCART_1:85
.=
gg `11
by A63
;
A70:
o2 =
[[o1,o2],[g1,h1]] `12
by MCART_1:85
.=
gg `12
by A63
;
A71:
g1 =
[[o1,o2],[g1,h1]] `21
by MCART_1:85
.=
gg `21
by A63
;
A72:
h1 =
[[o1,o2],[g1,h1]] `22
by MCART_1:85
.=
gg `22
by A63
;
A73:
cod g = a
by A61, CAT_1:5;
A74:
cod g =
gg `12
by A3
.=
[[o1,o2],[g1,h1]] `12
by A63
.=
o2
by MCART_1:85
;
A75:
o2 =
a
by A61, CAT_1:5, A74
.=
[[c,d],f]
by A31
;
A76:
cod (gg `21) =
cod ([[o1,o2],[g1,h1]] `21)
by A63
.=
cod g1
by MCART_1:85
.=
o2 `11
by A64
.=
[[c,d],f] `11
by A75
.=
o `11
by A31
;
A77:
cod (gg `22) =
cod ([[o1,o2],[g1,h1]] `22)
by A63
.=
cod h1
by MCART_1:85
.=
o2 `12
by A65
.=
[[c,d],f] `12
by A75
.=
o `12
by A31
;
A78:
ii `11 =
[[o,o],[(id (o `11)),(id (o `12))]] `11
.=
cod g
by A73, MCART_1:85
.=
C9 . gg
.=
gg `12
by A3
;
A79:
ii `11 =
o
by MCART_1:85
.=
ii `12
by MCART_1:85
;
gg `12 = ii `11
by A78;
then A80:
[ii,gg] in dom (commaComp (F,G))
by A66;
hence i (*) g =
(commaComp (F,G)) . (
i,
g)
by CAT_1:def 1
.=
ii * gg
by A80, Def4
.=
[[(gg `11),(gg `12)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]]
by A1, A79, Def3, A78
.=
[[(gg `11),(gg `12)],[(gg `21),((ii `22) (*) (gg `22))]]
by A76, CAT_1:21, A67
.=
[[(gg `11),(gg `12)],[(gg `21),(gg `22)]]
by CAT_1:21, A68, A77
.=
g
by A69, A70, A71, A72, A63
;
verum
end;
end;
A81:
for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #);
( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A82:
dom g = cod f
;
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider f1 =
f,
g1 =
g as
Element of
commaMorphs (
F,
G) ;
A83:
(
dom g = g1 `11 &
cod f = f1 `12 )
by A2, A3;
then
[g1,f1] in dom a9
by A4, A82;
then A84:
(
g (*) f = a9 . (
g,
f) &
a9 . (
g1,
f1)
= g1 * f1 )
by Def4, CAT_1:def 1;
A85:
(
dom f = f `11 &
cod g = g `12 )
by A2, A3;
A86:
(
dom (g (*) f) = (g (*) f) `11 &
cod (g (*) f) = (g (*) f) `12 )
by A2, A3;
g1 * f1 = [[(f1 `11),(g1 `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]]
by A1, A82, A83, Def3;
hence
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
by A86, A85, A84, MCART_1:85;
verum
end;
A87:
for f, g, h being Morphism of CatStr(# O,M,D9,C9,a9 #) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let f,
g,
h be
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #);
( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f1 =
f,
g1 =
g,
h1 =
h,
gf =
g (*) f,
hg =
h (*) g as
Element of
commaMorphs (
F,
G) ;
assume that A88:
dom h = cod g
and A89:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
A90:
(
dom g = g `11 &
cod g = g `12 )
by A2, A3;
dom (h (*) g) = dom g
by A81, A88;
then A91:
(h (*) g) (*) f = [[(f `11),(hg `12)],[((hg `21) (*) (f1 `21)),((hg `22) (*) (f1 `22))]]
by A5, A89;
A92:
(
dom h = h `11 &
cod f = f `12 )
by A2, A3;
cod (g (*) f) = cod g
by A81, A89;
then A93:
h (*) (g (*) f) = [[(gf `11),(h `12)],[((h1 `21) (*) (gf `21)),((h1 `22) (*) (gf `22))]]
by A5, A88;
A94:
(
dom (h1 `21) = (h1 `11) `11 &
cod (f1 `21) = (f1 `12) `11 )
by A1, Th2;
A95:
(
dom (h1 `22) = (h1 `11) `12 &
cod (f1 `22) = (f1 `12) `12 )
by A1, Th2;
A96:
(
dom (g1 `22) = (g1 `11) `12 &
cod (g1 `22) = (g1 `12) `12 )
by A1, Th2;
A97:
h (*) g = [[(g `11),(h `12)],[((h1 `21) (*) (g1 `21)),((h1 `22) (*) (g1 `22))]]
by A5, A88;
then A98:
(
(h (*) g) `12 = h `12 &
hg `21 = (h1 `21) (*) (g1 `21) )
by MCART_1:85;
A99:
g (*) f = [[(f `11),(g `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]]
by A5, A89;
then A100:
(
(g (*) f) `11 = f `11 &
gf `21 = (g1 `21) (*) (f1 `21) )
by MCART_1:85;
A101:
gf `22 = (g1 `22) (*) (f1 `22)
by A99, MCART_1:85;
A102:
hg `22 = (h1 `22) (*) (g1 `22)
by A97, MCART_1:85;
(
dom (g1 `21) = (g1 `11) `11 &
cod (g1 `21) = (g1 `12) `11 )
by A1, Th2;
then
((h1 `21) (*) (g1 `21)) (*) (f1 `21) = (h1 `21) (*) ((g1 `21) (*) (f1 `21))
by A88, A89, A90, A94, A92, CAT_1:18;
hence
h (*) (g (*) f) = (h (*) g) (*) f
by A88, A89, A90, A92, A96, A95, A93, A91, A98, A100, A102, A101, CAT_1:18;
verum
end;
for f, g being Morphism of CatStr(# O,M,D9,C9,a9 #) holds
( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f )
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
D9,
C9,
a9 #);
( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) iff dom g = cod f )
reconsider f1 =
f,
g1 =
g as
Element of
commaMorphs (
F,
G) ;
A103:
(
dom g = g1 `11 &
cod f = f1 `12 )
by A2, A3;
thus
(
[g,f] in dom the
Comp of
CatStr(#
O,
M,
D9,
C9,
a9 #) implies
dom g = cod f )
( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9 #) )proof
assume
[g,f] in dom the
Comp of
CatStr(#
O,
M,
D9,
C9,
a9 #)
;
dom g = cod f
then consider k1,
k2 being
Element of
commaMorphs (
F,
G)
such that A104:
[g,f] = [k1,k2]
and A105:
k1 `11 = k2 `12
by A4;
g = k1
by A104, XTUPLE_0:1;
hence
dom g = cod f
by A103, A104, A105, XTUPLE_0:1;
verum
end;
thus
(
dom g = cod f implies
[g,f] in dom the
Comp of
CatStr(#
O,
M,
D9,
C9,
a9 #) )
by A4, A103;
verum
end;
then reconsider FG = CatStr(# O,M,D9,C9,a9 #) as strict Category by A81, A87, A11, A26, CAT_1:def 6, CAT_1:def 7, CAT_1:def 8, CAT_1:def 9, CAT_1:def 10;
take
FG
; ( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) )
thus
( the carrier of FG = commaObjs (F,G) & the carrier' of FG = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of FG . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of FG . k = k `12 ) & the Comp of FG = commaComp (F,G) )
by A2, A3; verum