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
;
A13:
cod g = o `11
;
A14:
dom h = o `12
;
A15:
cod h = o `12
;
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 = o `11
by A16, MCART_1:85;
A21:
d = o `12
by A16, MCART_1:85;
A22:
cod (o `2) =
cod f
by A16
.=
G . d
by A17, CAT_1:1
.=
G . (o `12)
by A21
;
dom (o `2) =
F . c
by A16, A17, CAT_1:1
.=
F . (o `11)
by A20
;
then A23:
(o `2) (*) (F . g) =
o `2
by A18, CAT_1:22
.=
(G . h) (*) (o `2)
by A19, A22, 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, A23;
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 #) ;
A24:
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 A24;
hence
Hom (
b,
b)
<> {}
;
verum
end;
A25:
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 ;
A26:
dom g = o `11
;
A27:
cod g = o `11
;
A28:
dom h = o `12
;
A29:
cod h = o `12
;
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 A30:
o = [[c,d],f]
and A31:
f in Hom (
(F . c),
(G . d))
;
A32:
F . g = id (F . (o `11))
by CAT_1:71;
A33:
G . h = id (G . (o `12))
by CAT_1:71;
A34:
c = o `11
by A30, MCART_1:85;
A35:
d = o `12
by A30, MCART_1:85;
A36:
cod (o `2) =
cod f
by A30
.=
G . d
by A31, CAT_1:1
.=
G . (o `12)
by A35
;
dom (o `2) =
F . c
by A30, A31, CAT_1:1
.=
F . (o `11)
by A34
;
then A37:
(o `2) (*) (F . g) =
o `2
by A32, CAT_1:22
.=
(G . h) (*) (o `2)
by A33, A36, 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 A26, A27, A28, A29, A37;
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 #) ;
A38:
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 A38;
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 A39:
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) ;
A40:
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 A41:
gg = [[o1,o2],[g1,h1]]
and A42:
dom g1 = o1 `11
and
cod g1 = o2 `11
and A43:
dom h1 = o1 `12
and
(
cod h1 = o2 `12 &
(o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2) )
by A40;
A44:
dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 }
by Def4;
A45:
ii `21 =
[[o,o],[(id (o `11)),(id (o `12))]] `21
.=
id (o `11)
by MCART_1:85
;
A46:
ii `22 =
[[o,o],[(id (o `11)),(id (o `12))]] `22
.=
id (o `12)
by MCART_1:85
;
A47:
o1 =
[[o1,o2],[g1,h1]] `11
by MCART_1:85
.=
gg `11
by A41
;
A48:
o2 =
[[o1,o2],[g1,h1]] `12
by MCART_1:85
.=
gg `12
by A41
;
A49:
g1 =
[[o1,o2],[g1,h1]] `21
by MCART_1:85
.=
gg `21
by A41
;
A50:
h1 =
[[o1,o2],[g1,h1]] `22
by MCART_1:85
.=
gg `22
by A41
;
A51:
dom g = a
by A39, CAT_1:5;
A52:
dom g =
gg `11
by A2
.=
[[o1,o2],[g1,h1]] `11
by A41
.=
o1
by MCART_1:85
;
A53:
o1 =
a
by A39, A52, CAT_1:5
.=
[[c,d],f]
by A30
;
A54:
dom (gg `21) =
dom ([[o1,o2],[g1,h1]] `21)
by A41
.=
dom g1
by MCART_1:85
.=
o1 `11
by A42
.=
[[c,d],f] `11
by A53
.=
o `11
by A30
;
A55:
dom (gg `22) =
dom ([[o1,o2],[g1,h1]] `22)
by A41
.=
dom h1
by MCART_1:85
.=
o1 `12
by A43
.=
[[c,d],f] `12
by A53
.=
o `12
by A30
;
A56:
ii `11 =
[[o,o],[(id (o `11)),(id (o `12))]] `11
.=
dom g
by A51, MCART_1:85
.=
D9 . gg
.=
gg `11
by A2
;
A57:
ii `11 =
o
by MCART_1:85
.=
ii `12
by MCART_1:85
;
then
gg `11 = ii `12
by A56;
then A58:
[gg,ii] in dom (commaComp (F,G))
by A44;
hence g (*) i =
(commaComp (F,G)) . (
g,
i)
by CAT_1:def 1
.=
gg * ii
by A58, Def4
.=
[[(gg `11),(gg `12)],[((gg `21) (*) (id (o `11))),((gg `22) (*) (ii `22))]]
by A1, A57, Def3, A56, A45
.=
[[(gg `11),(gg `12)],[(gg `21),((gg `22) (*) (ii `22))]]
by A54, CAT_1:22
.=
[[(gg `11),(gg `12)],[(gg `21),(gg `22)]]
by A46, A55, CAT_1:22
.=
g
by A47, A48, A49, A50, A41
;
verum
end;
thus
(
Hom (
b,
a)
<> {} implies for
f being
Morphism of
b,
a holds
i (*) f = f )
verumproof
assume A59:
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) ;
A60:
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 A61:
gg = [[o1,o2],[g1,h1]]
and
dom g1 = o1 `11
and A62:
cod g1 = o2 `11
and
dom h1 = o1 `12
and A63:
cod h1 = o2 `12
and
(o2 `2) (*) (F . g1) = (G . h1) (*) (o1 `2)
by A60;
A64:
dom (commaComp (F,G)) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 }
by Def4;
A65:
ii `21 =
[[o,o],[(id (o `11)),(id (o `12))]] `21
.=
id (o `11)
by MCART_1:85
;
A66:
ii `22 =
[[o,o],[(id (o `11)),(id (o `12))]] `22
.=
id (o `12)
by MCART_1:85
;
A67:
o1 =
[[o1,o2],[g1,h1]] `11
by MCART_1:85
.=
gg `11
by A61
;
A68:
o2 =
[[o1,o2],[g1,h1]] `12
by MCART_1:85
.=
gg `12
by A61
;
A69:
g1 =
[[o1,o2],[g1,h1]] `21
by MCART_1:85
.=
gg `21
by A61
;
A70:
h1 =
[[o1,o2],[g1,h1]] `22
by MCART_1:85
.=
gg `22
by A61
;
A71:
cod g = a
by A59, CAT_1:5;
A72:
cod g =
gg `12
by A3
.=
[[o1,o2],[g1,h1]] `12
by A61
.=
o2
by MCART_1:85
;
A73:
o2 =
a
by A59, A72, CAT_1:5
.=
[[c,d],f]
by A30
;
A74:
cod (gg `21) =
cod ([[o1,o2],[g1,h1]] `21)
by A61
.=
cod g1
by MCART_1:85
.=
o2 `11
by A62
.=
[[c,d],f] `11
by A73
.=
o `11
by A30
;
A75:
cod (gg `22) =
cod ([[o1,o2],[g1,h1]] `22)
by A61
.=
cod h1
by MCART_1:85
.=
o2 `12
by A63
.=
[[c,d],f] `12
by A73
.=
o `12
by A30
;
A76:
ii `11 =
[[o,o],[(id (o `11)),(id (o `12))]] `11
.=
cod g
by A71, MCART_1:85
.=
C9 . gg
.=
gg `12
by A3
;
A77:
ii `11 =
o
by MCART_1:85
.=
ii `12
by MCART_1:85
;
gg `12 = ii `11
by A76;
then A78:
[ii,gg] in dom (commaComp (F,G))
by A64;
hence i (*) g =
(commaComp (F,G)) . (
i,
g)
by CAT_1:def 1
.=
ii * gg
by A78, Def4
.=
[[(gg `11),(gg `12)],[((ii `21) (*) (gg `21)),((ii `22) (*) (gg `22))]]
by A1, A77, Def3, A76
.=
[[(gg `11),(gg `12)],[(gg `21),((ii `22) (*) (gg `22))]]
by A74, A65, CAT_1:21
.=
[[(gg `11),(gg `12)],[(gg `21),(gg `22)]]
by A66, A75, CAT_1:21
.=
g
by A67, A68, A69, A70, A61
;
verum
end;
end;
A79:
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 A80:
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) ;
A81:
(
dom g = g1 `11 &
cod f = f1 `12 )
by A2, A3;
then
[g1,f1] in dom a9
by A4, A80;
then A82:
(
g (*) f = a9 . (
g,
f) &
a9 . (
g1,
f1)
= g1 * f1 )
by Def4, CAT_1:def 1;
A83:
(
dom f = f `11 &
cod g = g `12 )
by A2, A3;
A84:
(
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, A80, A81, Def3;
hence
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
by A84, A83, A82, MCART_1:85;
verum
end;
A85:
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 A86:
dom h = cod g
and A87:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
A88:
(
dom g = g `11 &
cod g = g `12 )
by A2, A3;
dom (h (*) g) = dom g
by A79, A86;
then A89:
(h (*) g) (*) f = [[(f `11),(hg `12)],[((hg `21) (*) (f1 `21)),((hg `22) (*) (f1 `22))]]
by A5, A87;
A90:
(
dom h = h `11 &
cod f = f `12 )
by A2, A3;
cod (g (*) f) = cod g
by A79, A87;
then A91:
h (*) (g (*) f) = [[(gf `11),(h `12)],[((h1 `21) (*) (gf `21)),((h1 `22) (*) (gf `22))]]
by A5, A86;
A92:
(
dom (h1 `21) = (h1 `11) `11 &
cod (f1 `21) = (f1 `12) `11 )
by A1, Th2;
A93:
(
dom (h1 `22) = (h1 `11) `12 &
cod (f1 `22) = (f1 `12) `12 )
by A1, Th2;
A94:
(
dom (g1 `22) = (g1 `11) `12 &
cod (g1 `22) = (g1 `12) `12 )
by A1, Th2;
A95:
h (*) g = [[(g `11),(h `12)],[((h1 `21) (*) (g1 `21)),((h1 `22) (*) (g1 `22))]]
by A5, A86;
then A96:
(
(h (*) g) `12 = h `12 &
hg `21 = (h1 `21) (*) (g1 `21) )
by MCART_1:85;
A97:
g (*) f = [[(f `11),(g `12)],[((g1 `21) (*) (f1 `21)),((g1 `22) (*) (f1 `22))]]
by A5, A87;
then A98:
(
(g (*) f) `11 = f `11 &
gf `21 = (g1 `21) (*) (f1 `21) )
by MCART_1:85;
A99:
gf `22 = (g1 `22) (*) (f1 `22)
by A97, MCART_1:85;
A100:
hg `22 = (h1 `22) (*) (g1 `22)
by A95, 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 A86, A87, A88, A92, A90, CAT_1:18;
hence
h (*) (g (*) f) = (h (*) g) (*) f
by A86, A87, A88, A90, A94, A93, A91, A89, A96, A98, A100, A99, 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) ;
A101:
(
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 A102:
[g,f] = [k1,k2]
and A103:
k1 `11 = k2 `12
by A4;
g = k1
by A102, XTUPLE_0:1;
hence
dom g = cod f
by A101, A102, A103, 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, A101;
verum
end;
then reconsider FG = CatStr(# O,M,D9,C9,a9 #) as strict Category by A79, A85, A11, A25, 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