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:44;
( dom (o `2 ) = F . (o `11 ) & F . (id (o `11 )) = id (F . (o `11 )) ) by A1, Th2, CAT_1:108;
then A6: (o `2 ) * (F . (id (o `11 ))) = o `2 by CAT_1:47;
( cod (o `2 ) = G . (o `12 ) & G . (id (o `12 )) = id (G . (o `12 )) ) by A1, Th2, CAT_1:108;
then A7: (G . (id (o `12 ))) * (o `2 ) = o `2 by CAT_1:46;
( dom (id (o `11 )) = o `11 & cod (id (o `11 )) = o `11 ) by CAT_1:44;
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 4;
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:89;
A20: (I . b9) `12 = b9 by A18, MCART_1:89;
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:89;
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:46;
cod (f9 `21 ) = (f9 `12 ) `11 by A1, Th3;
then A25: (id (b9 `11 )) * (f9 `21 ) = f9 `21 by A23, CAT_1:46;
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:47;
dom (g9 `21 ) = (g9 `11 ) `11 by A1, Th3;
then A29: (g9 `21 ) * (id (b9 `11 )) = g9 `21 by A27, CAT_1:47;
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 4;
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:89; :: 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:89;
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:89;
A50: gf `22 = (g1 `22 ) * (f1 `22 ) by A48, MCART_1:89;
A51: hg `22 = (h1 `22 ) * (g1 `22 ) by A46, MCART_1:89;
( 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:43;
hence h * (g * f) = (h * g) * f by A37, A38, A39, A41, A45, A44, A42, A40, A47, A49, A51, A50, CAT_1:43; :: 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:33;
hence dom g = cod f by A52, A53, A54, ZFMISC_1:33; :: 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:29;
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: