reconsider O = commaObjs (F,G), M = commaMorphs (F,G) as non empty set ;
defpred S₁[ Element of commaObjs (F,G), set ] means $2 = [[$1,$1],[(id ($1 `11)),(id ($1 `12))]];
deffunc H₃( Element of commaMorphs (F,G)) -> Element of commaObjs (F,G) = $1 `12 ;
deffunc H₄( 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 = H₄(k) from FUNCT_2:sch 4();
A3: commaMorphs (F,G) = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs (F,G) : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2) * (F . g) = (G . h) * (o1 `2) ) } by A1, Def6;
A4: for o being Element of commaObjs (F,G) ex k being Element of commaMorphs (F,G) st S₁[o,k]

let o be Element of commaObjs (F,G); :: thesis:
A5: ( dom (id (o `12)) = o `12 & cod (id (o `12)) = o `12 ) by CAT_1:19;
( dom (o `2) = F . (o `11) & F . (id (o `11)) = id (F . (o `11)) ) by A1, Th2, CAT_1:71;
then A6: (o `2) * (F . (id (o `11))) = o `2 by CAT_1:22;
( cod (o `2) = G . (o `12) & G . (id (o `12)) = id (G . (o `12)) ) by A1, Th2, CAT_1:71;
then A7: (G . (id (o `12))) * (o `2) = o `2 by CAT_1:21;
( dom (id (o `11)) = o `11 & cod (id (o `11)) = o `11 ) by CAT_1:19;
then [[o,o],[(id (o `11)),(id (o `12))]] in commaMorphs (F,G) by A3, A5, A6, A7;
hence ex k being Element of commaMorphs (F,G) st S₁[o,k] ; :: thesis:

end;

consider I being Function of (commaObjs (F,G)),(commaMorphs (F,G)) such that
A8: for o being Element of commaObjs (F,G) holds S₁[o,I . o] from FUNCT_2:sch 3(A4);
reconsider I = I 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
A9: for k being Element of commaMorphs (F,G) holds C9 . k = H₃(k) from FUNCT_2:sch 4();
reconsider D9 = D9, C9 = C9 as Function of M,O ;
set FG = CatStr(# O,M,D9,C9,a9,I #);
A10: dom the Comp of CatStr(# O,M,D9,C9,a9,I #) = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by Def8;
A11: for f, g being Morphism of CatStr(# O,M,D9,C9,a9,I #)
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,I #); :: thesis:
let k1, k2 be Element of commaMorphs (F,G); :: thesis:
assume that
A12: ( f = k1 & g = k2 ) and
A13: dom g = cod f ; :: thesis:
A14: ( dom g = k2 `11 & cod f = k1 `12 ) by A2, A9, A12;
then A15: [k2,k1] in dom a9 by A10, A13;
then A16: a9 . (k2,k1) = k2 * k1 by Def8;
g * f = a9 . (g,f) by A12, A15, CAT_1:def 1;
hence g * f = [[(k1 `11),(k2 `12)],[((k2 `21) * (k1 `21)),((k2 `22) * (k1 `22))]] by A1, A12, A13, A14, A16, Def7; :: thesis:

end;

A17: for b being Object of CatStr(# O,M,D9,C9,a9,I #) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of CatStr(# O,M,D9,C9,a9,I #) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of CatStr(# O,M,D9,C9,a9,I #) st dom g = b holds
g * (id b) = g ) )

proof

let b be Object of CatStr(# O,M,D9,C9,a9,I #); :: thesis:
reconsider b9 = b as Element of commaObjs (F,G) ;
reconsider i = id b as Element of commaMorphs (F,G) ;
A18: I . b9 = [[b9,b9],[(id (b9 `11)),(id (b9 `12))]] by A8;
then A19: (I . b9) `11 = b9 by MCART_1:85;
A20: (I . b9) `12 = b9 by A18, MCART_1:85;
hence ( dom (id b) = b & cod (id b) = b ) by A2, A9, A19; :: thesis:
A21: ( (I . b9) `21 = id (b9 `11) & (I . b9) `22 = id (b9 `12) ) by A18, MCART_1:85;
thus for f being Morphism of CatStr(# O,M,D9,C9,a9,I #) st cod f = b holds
(id b) * f = f :: thesis:

proof

let f be Morphism of CatStr(# O,M,D9,C9,a9,I #); :: thesis:
reconsider f9 = f as Element of commaMorphs (F,G) ;
assume A22: cod f = b ; :: thesis:
then A23: b = f `12 by A9;
cod (f9 `22) = (f9 `12) `12 by A1, Th3;
then A24: (id (b9 `12)) * (f9 `22) = f9 `22 by A23, CAT_1:21;
cod (f9 `21) = (f9 `12) `11 by A1, Th3;
then A25: (id (b9 `11)) * (f9 `21) = f9 `21 by A23, CAT_1:21;
cod f = dom (id b) by A2, A19, A22;
hence (id b) * f = [[(f9 `11),(i `12)],[((i `21) * (f9 `21)),((i `22) * (f9 `22))]] by A11
.= f by A1, A20, A21, A23, A25, A24, Th3 ;
:: thesis:

end;

let g be Morphism of CatStr(# O,M,D9,C9,a9,I #); :: thesis:
reconsider g9 = g as Element of commaMorphs (F,G) ;
assume A26: dom g = b ; :: thesis:
then A27: b = g `11 by A2;
dom (g9 `22) = (g9 `11) `12 by A1, Th3;
then A28: (g9 `22) * (id (b9 `12)) = g9 `22 by A27, CAT_1:22;
dom (g9 `21) = (g9 `11) `11 by A1, Th3;
then A29: (g9 `21) * (id (b9 `11)) = g9 `21 by A27, CAT_1:22;
dom g = cod (id b) by A9, A20, A26;
hence g * (id b) = [[(i `11),(g9 `12)],[((g9 `21) * (i `21)),((g9 `22) * (i `22))]] by A11
.= g by A1, A19, A21, A27, A29, A28, Th3 ;
:: thesis:

end;

A30: for f, g being Morphism of CatStr(# O,M,D9,C9,a9,I #) 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,I #); :: thesis:
assume A31: dom g = cod f ; :: thesis:
reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ;
A32: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A9;
then [g1,f1] in dom a9 by A10, A31;
then A33: ( g * f = a9 . (g,f) & a9 . (g1,f1) = g1 * f1 ) by Def8, CAT_1:def 1;
A34: ( dom f = f `11 & cod g = g `12 ) by A2, A9;
A35: ( dom (g * f) = (g * f) `11 & cod (g * f) = (g * f) `12 ) by A2, A9;
g1 * f1 = [[(f1 `11),(g1 `12)],[((g1 `21) * (f1 `21)),((g1 `22) * (f1 `22))]] by A1, A31, A32, Def7;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by A35, A34, A33, MCART_1:85; :: thesis:

end;

A36: for f, g, h being Morphism of CatStr(# O,M,D9,C9,a9,I #) 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,I #); :: thesis:
reconsider f1 = f, g1 = g, h1 = h, gf = g * f, hg = h * g as Element of commaMorphs (F,G) ;
assume that
A37: dom h = cod g and
A38: dom g = cod f ; :: thesis:
A39: ( dom g = g `11 & cod g = g `12 ) by A2, A9;
dom (h * g) = dom g by A30, A37;
then A40: (h * g) * f = [[(f `11),(hg `12)],[((hg `21) * (f1 `21)),((hg `22) * (f1 `22))]] by A11, A38;
A41: ( dom h = h `11 & cod f = f `12 ) by A2, A9;
cod (g * f) = cod g by A30, A38;
then A42: h * (g * f) = [[(gf `11),(h `12)],[((h1 `21) * (gf `21)),((h1 `22) * (gf `22))]] by A11, A37;
A43: ( dom (h1 `21) = (h1 `11) `11 & cod (f1 `21) = (f1 `12) `11 ) by A1, Th3;
A44: ( dom (h1 `22) = (h1 `11) `12 & cod (f1 `22) = (f1 `12) `12 ) by A1, Th3;
A45: ( dom (g1 `22) = (g1 `11) `12 & cod (g1 `22) = (g1 `12) `12 ) by A1, Th3;
A46: h * g = [[(g `11),(h `12)],[((h1 `21) * (g1 `21)),((h1 `22) * (g1 `22))]] by A11, A37;
then A47: ( (h * g) `12 = h `12 & hg `21 = (h1 `21) * (g1 `21) ) by MCART_1:85;
A48: g * f = [[(f `11),(g `12)],[((g1 `21) * (f1 `21)),((g1 `22) * (f1 `22))]] by A11, A38;
then A49: ( (g * f) `11 = f `11 & gf `21 = (g1 `21) * (f1 `21) ) by MCART_1:85;
A50: gf `22 = (g1 `22) * (f1 `22) by A48, MCART_1:85;
A51: hg `22 = (h1 `22) * (g1 `22) by A46, MCART_1:85;
( dom (g1 `21) = (g1 `11) `11 & cod (g1 `21) = (g1 `12) `11 ) by A1, Th3;
then ((h1 `21) * (g1 `21)) * (f1 `21) = (h1 `21) * ((g1 `21) * (f1 `21)) by A37, A38, A39, A43, A41, CAT_1:18;
hence h * (g * f) = (h * g) * f by A37, A38, A39, A41, A45, A44, A42, A40, A47, A49, A51, A50, CAT_1:18; :: thesis:

end;

for f, g being Morphism of CatStr(# O,M,D9,C9,a9,I #) holds
( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9,I #) iff dom g = cod f )

proof

let f, g be Morphism of CatStr(# O,M,D9,C9,a9,I #); :: thesis:
reconsider f1 = f, g1 = g as Element of commaMorphs (F,G) ;
A52: ( dom g = g1 `11 & cod f = f1 `12 ) by A2, A9;
thus ( [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9,I #) implies dom g = cod f ) :: thesis:

proof

assume [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9,I #) ; :: thesis:
then consider k1, k2 being Element of commaMorphs (F,G) such that
A53: [g,f] = [k1,k2] and
A54: k1 `11 = k2 `12 by A10;
g = k1 by A53, ZFMISC_1:27;
hence dom g = cod f by A52, A53, A54, ZFMISC_1:27; :: thesis:

end;

thus ( dom g = cod f implies [g,f] in dom the Comp of CatStr(# O,M,D9,C9,a9,I #) ) by A10, A52; :: thesis:

end;

then reconsider FG = CatStr(# O,M,D9,C9,a9,I #) as strict Category by A30, A36, A17, CAT_1:10;
take FG ; :: thesis:
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 ) & ( for o being Element of commaObjs (F,G) holds the Id of FG . o = [[o,o],[(id (o `11)),(id (o `12))]] ) & the Comp of FG = commaComp (F,G) ) by A2, A9, A8; :: thesis: