set DD = the Source of C1 | the carrier' of C2;
set CC = the Target of C1 | the carrier' of C2;
set Cm = the Comp of C1 || the carrier' of C2;
set I = the Id of C1 | the carrier of C2;
reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set by A3, XBOOLE_0:def 4;
reconsider o2 = o1 as Object of C2 by A3;
reconsider o = o1 as Object of C by A1, CAT_2:12;
A4: id o1 = id o by A1, CAT_2:def 4;
id o2 = id o by A2, CAT_2:def 4;
then reconsider M = the carrier' of C1 /\ the carrier' of C2 as non empty set by A4, XBOOLE_0:def 4;
A5: dom the Id of C1 = the carrier of C1 by FUNCT_2:def 1;
A6: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A7: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A8: dom (the Source of C1 | the carrier' of C2) = M by A6, RELAT_1:90;
A9: dom (the Target of C1 | the carrier' of C2) = M by A7, RELAT_1:90;
A10: dom (the Id of C1 | the carrier of C2) = O by A5, RELAT_1:90;
rng (the Source of C1 | the carrier' of C2) c= O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (the Source of C1 | the carrier' of C2) ; :: thesis:
then consider m being set such that
A11: m in dom (the Source of C1 | the carrier' of C2) and
A12: x = (the Source of C1 | the carrier' of C2) . m by FUNCT_1:def 5;
reconsider m1 = m as Morphism of C1 by A11;
reconsider m2 = m as Morphism of C2 by A8, A11, XBOOLE_0:def 4;
reconsider m = m1 as Morphism of C by A1, CAT_2:14;
A13: x = dom m1 by A11, A12, FUNCT_1:70;
A14: dom m1 = dom m by A1, CAT_2:15;
dom m = dom m2 by A2, CAT_2:15;
hence x in O by A13, A14, XBOOLE_0:def 4; :: thesis:

end;

then reconsider DD = the Source of C1 | the carrier' of C2 as Function of M,O by A8, FUNCT_2:def 1, RELSET_1:11;
rng (the Target of C1 | the carrier' of C2) c= O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (the Target of C1 | the carrier' of C2) ; :: thesis:
then consider m being set such that
A15: m in dom (the Target of C1 | the carrier' of C2) and
A16: x = (the Target of C1 | the carrier' of C2) . m by FUNCT_1:def 5;
reconsider m1 = m as Morphism of C1 by A15;
reconsider m2 = m as Morphism of C2 by A9, A15, XBOOLE_0:def 4;
reconsider m = m1 as Morphism of C by A1, CAT_2:14;
A17: x = cod m1 by A15, A16, FUNCT_1:70;
A18: cod m1 = cod m by A1, CAT_2:15;
cod m = cod m2 by A2, CAT_2:15;
hence x in O by A17, A18, XBOOLE_0:def 4; :: thesis:

end;

then reconsider CC = the Target of C1 | the carrier' of C2 as Function of M,O by A9, FUNCT_2:def 1, RELSET_1:11;
rng (the Id of C1 | the carrier of C2) c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (the Id of C1 | the carrier of C2) ; :: thesis:
then consider m being set such that
A19: m in dom (the Id of C1 | the carrier of C2) and
A20: x = (the Id of C1 | the carrier of C2) . m by FUNCT_1:def 5;
reconsider m1 = m as Object of C1 by A19;
reconsider m2 = m as Object of C2 by A10, A19, XBOOLE_0:def 4;
reconsider m = m1 as Object of C by A1, CAT_2:12;
A21: x = id m1 by A19, A20, FUNCT_1:70;
A22: id m1 = id m by A1, CAT_2:def 4;
id m = id m2 by A2, CAT_2:def 4;
hence x in M by A21, A22, XBOOLE_0:def 4; :: thesis:

end;

then reconsider I = the Id of C1 | the carrier of C2 as Function of O,M by A10, FUNCT_2:def 1, RELSET_1:11;
A23: dom (the Comp of C1 || the carrier' of C2) = (dom the Comp of C1) /\ [:the carrier' of C2,the carrier' of C2:] by RELAT_1:90;
then dom (the Comp of C1 || the carrier' of C2) c= [:the carrier' of C1,the carrier' of C1:] /\ [:the carrier' of C2,the carrier' of C2:] by XBOOLE_1:26;
then A24: dom (the Comp of C1 || the carrier' of C2) c= [:M,M:] by ZFMISC_1:123;
rng (the Comp of C1 || the carrier' of C2) c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (the Comp of C1 || the carrier' of C2) ; :: thesis:
then consider m being set such that
A25: m in dom (the Comp of C1 || the carrier' of C2) and
A26: x = (the Comp of C1 || the carrier' of C2) . m by FUNCT_1:def 5;
A27: m `1 in M by A24, A25, MCART_1:10;
A28: m `2 in M by A24, A25, MCART_1:10;
A29: m = [(m `1 ),(m `2 )] by A24, A25, MCART_1:23;
reconsider m1 = m `1 , m2 = m `2 as Morphism of C1 by A27, A28, XBOOLE_0:def 4;
reconsider n1 = m `1 , n2 = m `2 as Morphism of C2 by A27, A28, XBOOLE_0:def 4;
reconsider mm = m1, n = m2 as Morphism of C by A1, CAT_2:14;
A30: m in dom the Comp of C1 by A23, A25, XBOOLE_0:def 4;
then A31: dom m1 = cod m2 by A29, CAT_1:40;
A32: x = the Comp of C1 . m1,m2 by A25, A26, A29, FUNCT_1:70;
A33: dom m1 = dom mm by A1, CAT_2:15;
A34: dom n1 = dom mm by A2, CAT_2:15;
A35: cod m2 = cod n by A1, CAT_2:15;
A36: cod n2 = cod n by A2, CAT_2:15;
A37: x = m1 * m2 by A29, A30, A32, CAT_1:def 4;
A38: m1 * m2 = mm * n by A1, A31, CAT_2:17;
mm * n = n1 * n2 by A2, A31, A33, A34, A35, A36, CAT_2:17;
hence x in M by A37, A38, XBOOLE_0:def 4; :: thesis:

end;

then reconsider Cm = the Comp of C1 || the carrier' of C2 as PartFunc of [:M,M:],M by A24, RELSET_1:11;
set CAT = CatStr(# O,M,DD,CC,Cm,I #);
CatStr(# O,M,DD,CC,Cm,I #) is Category-like

proof

hereby :: according to CAT_1:def 8 :: thesis:

let f, g be Morphism of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
A40: g in the carrier' of C2 by XBOOLE_0:def 4;
A41: f in the carrier' of C2 by XBOOLE_0:def 4;

hereby :: thesis:

assume [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) ; :: thesis:
then A42: [g,f] in dom the Comp of C1 by A23, XBOOLE_0:def 4;
thus the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Source of C1 . g9 by A40, FUNCT_1:72
.= the Target of C1 . f9 by A42, CAT_1:def 8
.= the Target of CatStr(# O,M,DD,CC,Cm,I #) . f by A41, FUNCT_1:72 ; :: thesis:

end;

assume A43: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Target of CatStr(# O,M,DD,CC,Cm,I #) . f ; :: thesis:
A44: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Source of C1 . g9 by A8, FUNCT_1:70;
A45: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Target of C1 . f9 by A9, A43, FUNCT_1:70;
A46: [g,f] in [:the carrier' of C2,the carrier' of C2:] by A40, A41, ZFMISC_1:106;
[g,f] in dom the Comp of C1 by A44, A45, CAT_1:def 8;
hence [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A23, A46, XBOOLE_0:def 4; :: thesis:

end;

hereby :: thesis:

let f, g be Morphism of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
assume A48: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Target of CatStr(# O,M,DD,CC,Cm,I #) . f ; :: thesis:
then A49: [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A39;
then reconsider h = the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,f as Morphism of CatStr(# O,M,DD,CC,Cm,I #) by PARTFUN1:27;
A50: h = the Comp of C1 . g9,f9 by A49, FUNCT_1:70;
A51: the Source of CatStr(# O,M,DD,CC,Cm,I #) . f = the Source of C1 . f9 by A8, FUNCT_1:70;
A52: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Source of C1 . g9 by A8, FUNCT_1:70;
A53: the Source of CatStr(# O,M,DD,CC,Cm,I #) . h = the Source of C1 . h by A8, FUNCT_1:70;
A54: the Target of CatStr(# O,M,DD,CC,Cm,I #) . f = the Target of C1 . f9 by A9, FUNCT_1:70;
A55: the Target of CatStr(# O,M,DD,CC,Cm,I #) . g = the Target of C1 . g9 by A9, FUNCT_1:70;
the Target of CatStr(# O,M,DD,CC,Cm,I #) . h = the Target of C1 . h by A9, FUNCT_1:70;
hence ( the Source of CatStr(# O,M,DD,CC,Cm,I #) . (the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,f) = the Source of CatStr(# O,M,DD,CC,Cm,I #) . f & the Target of CatStr(# O,M,DD,CC,Cm,I #) . (the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,f) = the Target of CatStr(# O,M,DD,CC,Cm,I #) . g ) by A48, A50, A51, A52, A53, A54, A55, CAT_1:def 8; :: thesis:

end;

hereby :: thesis:

let f, g, h be Morphism of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider h9 = h, g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
assume that
A56: the Source of CatStr(# O,M,DD,CC,Cm,I #) . h = the Target of CatStr(# O,M,DD,CC,Cm,I #) . g and
A57: the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = the Target of CatStr(# O,M,DD,CC,Cm,I #) . f ; :: thesis:
A58: [h,g] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A39, A56;
A59: [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A39, A57;
then reconsider hg = the Comp of CatStr(# O,M,DD,CC,Cm,I #) . h,g, gf = the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,f as Morphism of CatStr(# O,M,DD,CC,Cm,I #) by A58, PARTFUN1:27;
reconsider hg9 = hg, gf9 = gf as Morphism of C1 by XBOOLE_0:def 4;
A60: the Source of CatStr(# O,M,DD,CC,Cm,I #) . hg = the Source of CatStr(# O,M,DD,CC,Cm,I #) . g by A47, A56;
A61: the Target of CatStr(# O,M,DD,CC,Cm,I #) . gf = the Target of CatStr(# O,M,DD,CC,Cm,I #) . g by A47, A57;
A62: [hg,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A39, A57, A60;
A63: [h,gf] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A39, A56, A61;
A64: the Source of C1 . h9 = the Source of CatStr(# O,M,DD,CC,Cm,I #) . h by A8, FUNCT_1:70;
A65: the Target of C1 . g9 = the Target of CatStr(# O,M,DD,CC,Cm,I #) . g by A9, FUNCT_1:70;
A66: the Source of C1 . g9 = the Source of CatStr(# O,M,DD,CC,Cm,I #) . g by A8, FUNCT_1:70;
A67: the Target of C1 . f9 = the Target of CatStr(# O,M,DD,CC,Cm,I #) . f by A9, FUNCT_1:70;
thus the Comp of CatStr(# O,M,DD,CC,Cm,I #) . h,(the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,f) = the Comp of C1 . [h9,gf9] by A63, FUNCT_1:70
.= the Comp of C1 . h9,(the Comp of C1 . g9,f9) by A59, FUNCT_1:70
.= the Comp of C1 . (the Comp of C1 . h9,g9),f9 by A56, A57, A64, A65, A66, A67, CAT_1:def 8
.= the Comp of C1 . [hg9,f9] by A58, FUNCT_1:70
.= the Comp of CatStr(# O,M,DD,CC,Cm,I #) . (the Comp of CatStr(# O,M,DD,CC,Cm,I #) . h,g),f by A62, FUNCT_1:70 ; :: thesis:

end;

let b be Object of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider b9 = b as Object of C1 by XBOOLE_0:def 4;
thus the Source of CatStr(# O,M,DD,CC,Cm,I #) . (the Id of CatStr(# O,M,DD,CC,Cm,I #) . b) = the Source of C1 . (the Id of CatStr(# O,M,DD,CC,Cm,I #) . b) by A8, FUNCT_1:70
.= the Source of C1 . (the Id of C1 . b9) by A10, FUNCT_1:70
.= b by CAT_1:def 8 ; :: thesis:
thus the Target of CatStr(# O,M,DD,CC,Cm,I #) . (the Id of CatStr(# O,M,DD,CC,Cm,I #) . b) = the Target of C1 . (the Id of CatStr(# O,M,DD,CC,Cm,I #) . b) by A9, FUNCT_1:70
.= the Target of C1 . (the Id of C1 . b9) by A10, FUNCT_1:70
.= b by CAT_1:def 8 ; :: thesis:

hereby :: thesis:

let f be Morphism of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider f9 = f as Morphism of C1 by XBOOLE_0:def 4;
assume the Target of CatStr(# O,M,DD,CC,Cm,I #) . f = b ; :: thesis:
then A68: the Target of C1 . f9 = b by A9, FUNCT_1:70;
A69: the Source of C1 . (the Id of C1 . b9) = b9 by CAT_1:def 8;
A70: the Id of C1 . b9 = the Id of CatStr(# O,M,DD,CC,Cm,I #) . b by A10, FUNCT_1:70;
A71: f in the carrier' of C2 by XBOOLE_0:def 4;
A72: the Id of CatStr(# O,M,DD,CC,Cm,I #) . b in the carrier' of C2 by XBOOLE_0:def 4;
A73: [(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b),f] in dom the Comp of C1 by A68, A69, A70, CAT_1:def 8;
A74: [(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b),f] in [:the carrier' of C2,the carrier' of C2:] by A71, A72, ZFMISC_1:106;
A75: the Comp of C1 . (the Id of C1 . b9),f9 = f9 by A68, CAT_1:def 8;
A76: [(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b),f] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A23, A73, A74, XBOOLE_0:def 4;
the Comp of C1 . [(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b),f] = f by A10, A75, FUNCT_1:70;
hence the Comp of CatStr(# O,M,DD,CC,Cm,I #) . (the Id of CatStr(# O,M,DD,CC,Cm,I #) . b),f = f by A76, FUNCT_1:70; :: thesis:

end;

let g be Morphism of CatStr(# O,M,DD,CC,Cm,I #); :: thesis:
reconsider g9 = g as Morphism of C1 by XBOOLE_0:def 4;
assume the Source of CatStr(# O,M,DD,CC,Cm,I #) . g = b ; :: thesis:
then A77: the Source of C1 . g9 = b9 by A8, FUNCT_1:70;
A78: the Target of C1 . (the Id of C1 . b9) = b9 by CAT_1:def 8;
A79: the Id of C1 . b9 = the Id of CatStr(# O,M,DD,CC,Cm,I #) . b by A10, FUNCT_1:70;
A80: g in the carrier' of C2 by XBOOLE_0:def 4;
A81: the Id of CatStr(# O,M,DD,CC,Cm,I #) . b in the carrier' of C2 by XBOOLE_0:def 4;
A82: [g,(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b)] in dom the Comp of C1 by A77, A78, A79, CAT_1:def 8;
A83: [g,(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b)] in [:the carrier' of C2,the carrier' of C2:] by A80, A81, ZFMISC_1:106;
A84: the Comp of C1 . g9,(the Id of C1 . b9) = g9 by A77, CAT_1:def 8;
A85: [g,(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b)] in dom the Comp of CatStr(# O,M,DD,CC,Cm,I #) by A23, A82, A83, XBOOLE_0:def 4;
the Comp of C1 . [g,(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b)] = g by A10, A84, FUNCT_1:70;
hence the Comp of CatStr(# O,M,DD,CC,Cm,I #) . g,(the Id of CatStr(# O,M,DD,CC,Cm,I #) . b) = g by A85, FUNCT_1:70; :: thesis:

end;

hence ex b₁ being strict Category st
( the carrier of b₁ = the carrier of C1 /\ the carrier of C2 & the carrier' of b₁ = the carrier' of C1 /\ the carrier' of C2 & the Source of b₁ = the Source of C1 | the carrier' of C2 & the Target of b₁ = the Target of C1 | the carrier' of C2 & the Comp of b₁ = the Comp of C1 || the carrier' of C2 & the Id of b₁ = the Id of C1 | the carrier of C2 ) ; :: thesis: