set M = { [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } ;
set a0 = the Element of F₁();
consider f0 being Element of F₂() such that
A4: P₁[ the Element of F₁(), the Element of F₁(),f0] and
for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[ the Element of F₁(),b,g] implies F₃(g,f0) = g ) & ( P₁[b, the Element of F₁(),g] implies F₃(f0,g) = g ) ) by A2;
A5: [[ the Element of F₁(), the Element of F₁()],f0] in { [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } by A4;
{ [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } c= [:[:F₁(),F₁():],F₂():]

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } ; :: thesis:
then ex a, b being Element of F₁() ex f being Element of F₂() st
( x = [[a,b],f] & P₁[a,b,f] ) ;
hence x in [:[:F₁(),F₁():],F₂():] ; :: thesis:

end;

then reconsider M = { [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } as non empty Subset of [:[:F₁(),F₁():],F₂():] by A5;

A6: now

let m be Element of M; :: thesis:
m in M ;
then consider a, b being Element of F₁(), f being Element of F₂() such that
A7: m = [[a,b],f] and
A8: P₁[a,b,f] ;
A9: m `11 = a by A7, MCART_1:85;
m `12 = b by A7, MCART_1:85;
hence ( m = [[(m `11),(m `12)],(m `2)] & P₁[m `11 ,m `12 ,m `2 ] ) by A7, A8, A9, MCART_1:7; :: thesis:

end;

deffunc H₁( Element of M) -> Element of F₁() = $1 `11 ;
consider DM being Function of M,F₁() such that
A10: for m being Element of M holds DM . m = H₁(m) from FUNCT_2:sch 4();
deffunc H₂( Element of M) -> Element of F₁() = $1 `12 ;
consider CM being Function of M,F₁() such that
A11: for m being Element of M holds CM . m = H₂(m) from FUNCT_2:sch 4();
deffunc H₃( set , set ) -> set = [[($2 `11),($1 `12)],F₃(($1 `2),($2 `2))];
defpred S₁[ set , set ] means ( $1 `11 = $2 `12 & $1 in M & $2 in M );

A12: now

let x, y be set ; :: thesis:
assume A13: S₁[x,y] ; :: thesis:
then consider ax, bx being Element of F₁(), fx being Element of F₂() such that
A14: x = [[ax,bx],fx] and
A15: P₁[ax,bx,fx] ;
consider ay, b2 being Element of F₁(), fy being Element of F₂() such that
A16: y = [[ay,b2],fy] and
A17: P₁[ay,b2,fy] by A13;
A18: x `11 = ax by A14, MCART_1:85;
A19: x `12 = bx by A14, MCART_1:85;
A20: y `11 = ay by A16, MCART_1:85;
A21: y `12 = b2 by A16, MCART_1:85;
A22: x `2 = fx by A14, MCART_1:7;
A23: y `2 = fy by A16, MCART_1:7;
A24: F₃(fx,fy) in F₂() by A1, A13, A15, A17, A18, A21;
P₁[ay,bx,F₃(fx,fy)] by A1, A13, A15, A17, A18, A21;
hence H₃(x,y) in M by A19, A20, A22, A23, A24; :: thesis:

end;

consider CC being PartFunc of [:M,M:],M such that
A25: for x, y being set holds
( [x,y] in dom CC iff ( x in M & y in M & S₁[x,y] ) ) and
A26: for x, y being set st [x,y] in dom CC holds
CC . (x,y) = H₃(x,y) from BINOP_1:sch 6(A12);
defpred S₂[ Element of F₁(), set ] means ex f being Element of F₂() st
( $2 = [[$1,$1],f] & P₁[$1,$1,f] & ( for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[$1,b,g] implies F₃(g,f) = g ) & ( P₁[b,$1,g] implies F₃(f,g) = g ) ) ) );

A27: now

let a be Element of F₁(); :: thesis:
consider f being Element of F₂() such that
A28: P₁[a,a,f] and
A29: for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[a,b,g] implies F₃(g,f) = g ) & ( P₁[b,a,g] implies F₃(f,g) = g ) ) by A2;
[[a,a],f] in M by A28;
then reconsider y = [[a,a],f] as Element of M ;
take y = y; :: thesis:
thus S₂[a,y] by A28, A29; :: thesis:

end;

consider I being Function of F₁(),M such that
A30: for o being Element of F₁() holds S₂[o,I . o] from FUNCT_2:sch 3(A27);
set C = CatStr(# F₁(),M,DM,CM,CC,I #);
CatStr(# F₁(),M,DM,CM,CC,I #) is Category-like

proof

hereby :: according to CAT_1:def 5 :: thesis:

let f, g be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
A31: ( [g,f] in dom CC iff ( g in M & f in M & g `11 = f `12 & g in M & f in M ) ) by A25;
DM . g = g `11 by A10;
hence ( [g,f] in dom the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) iff the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f ) by A11, A31; :: thesis:

end;

hereby :: thesis:

let f, g be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
A32: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `11 by A10;
A33: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `11 by A10;
A34: the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `12 by A11;
A35: the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `12 by A11;
assume the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f ; :: thesis:
then A36: [g,f] in dom CC by A25, A33, A34;
then A37: CC . (g,f) = [[(f `11),(g `12)],F₃((g `2),(f `2))] by A26;
A38: CC . (g,f) in rng CC by A36, FUNCT_1:def 3;
A39: (CC . [g,f]) `11 = f `11 by A37, MCART_1:85;
(CC . [g,f]) `12 = g `12 by A37, MCART_1:85;
hence ( the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . ( the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (g,f)) = the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . ( the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (g,f)) = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g ) by A10, A11, A32, A35, A38, A39; :: thesis:

end;

hereby :: thesis:

let f, g, h be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
A40: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `11 by A10;
A41: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . h = h `11 by A10;
A42: the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `12 by A11;
A43: the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `12 by A11;
assume that
A44: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . h = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g and
A45: the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f ; :: thesis:
A46: [g,f] in dom CC by A25, A40, A42, A45;
A47: [h,g] in dom CC by A25, A41, A43, A44;
A48: CC . [g,f] in rng CC by A46, FUNCT_1:def 3;
CC . [h,g] in rng CC by A47, FUNCT_1:def 3;
then reconsider gf = CC . (g,f), hg = CC . (h,g) as Element of M by A48;
A49: gf = [[(f `11),(g `12)],F₃((g `2),(f `2))] by A26, A46;
A50: hg = [[(g `11),(h `12)],F₃((h `2),(g `2))] by A26, A47;
A51: DM . gf = gf `11 by A10;
A52: DM . hg = hg `11 by A10;
A53: CM . gf = gf `12 by A11;
A54: CM . hg = hg `12 by A11;
A55: DM . gf = f `11 by A49, A51, MCART_1:85;
A56: DM . hg = g `11 by A50, A52, MCART_1:85;
A57: CM . gf = g `12 by A49, A53, MCART_1:85;
A58: CM . hg = h `12 by A50, A54, MCART_1:85;
A59: [h,gf] in dom CC by A25, A41, A43, A44, A53, A57;
A60: [hg,f] in dom CC by A25, A40, A42, A45, A52, A56;
reconsider f9 = f, g9 = g, h9 = h as Element of M ;
A61: P₁[f9 `11 ,f9 `12 ,f9 `2 ] by A6;
A62: P₁[g9 `11 ,g9 `12 ,g9 `2 ] by A6;
A63: P₁[h9 `11 ,h9 `12 ,h9 `2 ] by A6;
thus the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (h,( the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (g,f))) = [[(f `11),(h `12)],F₃((h `2),(gf `2))] by A26, A51, A55, A59
.= [[(f `11),(h `12)],F₃((h9 `2),F₃((g9 `2),(f9 `2)))] by A49, MCART_1:7
.= [[(f `11),(h `12)],F₃(F₃((h9 `2),(g9 `2)),(f9 `2))] by A3, A40, A41, A42, A43, A44, A45, A61, A62, A63
.= [[(f `11),(h `12)],F₃((hg `2),(f `2))] by A50, MCART_1:7
.= the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (( the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (h,g)),f) by A26, A54, A58, A60 ; :: thesis:

end;

let b be Object of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
consider f being Element of F₂() such that
A64: I . b = [[b,b],f] and
P₁[b,b,f] and
A65: for c being Element of F₁()
for g being Element of F₂() holds
( ( P₁[b,c,g] implies F₃(g,f) = g ) & ( P₁[c,b,g] implies F₃(f,g) = g ) ) by A30;
reconsider b9 = b as Element of F₁() ;
reconsider Ib = I . b9 as Element of M ;
thus the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . ( the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b) = (I . b) `11 by A10
.= b by A64, MCART_1:85 ; :: thesis:
thus the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . ( the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b) = (I . b) `12 by A11
.= b by A64, MCART_1:85 ; :: thesis:

hereby :: thesis:

let f9 be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
reconsider g = f9 as Element of M ;
assume the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f9 = b ; :: thesis:
then A66: g `12 = b by A11;
A67: Ib `11 = b by A64, MCART_1:85;
A68: P₁[g `11 ,b,g `2 ] by A6, A66;
A69: [Ib,g] in dom CC by A25, A66, A67;
A70: Ib `12 = b by A64, MCART_1:85;
A71: Ib `2 = f by A64, MCART_1:7;
A72: F₃(f,(g `2)) = g `2 by A65, A68;
CC . (Ib,g) = [[(g `11),b],F₃(f,(g `2))] by A26, A69, A70, A71;
hence the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (( the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b),f9) = f9 by A6, A66, A72; :: thesis:

end;

let f9 be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
reconsider g = f9 as Element of M ;
assume the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f9 = b ; :: thesis:
then A73: g `11 = b by A10;
A74: Ib `12 = b by A64, MCART_1:85;
A75: P₁[b,g `12 ,g `2 ] by A6, A73;
A76: [g,Ib] in dom CC by A25, A73, A74;
A77: Ib `11 = b by A64, MCART_1:85;
A78: Ib `2 = f by A64, MCART_1:7;
A79: F₃((g `2),f) = g `2 by A65, A75;
CC . (g,Ib) = [[b,(g `12)],F₃((g `2),f)] by A26, A76, A77, A78;
hence the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (f9,( the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b)) = f9 by A6, A73, A79; :: thesis:

end;

then reconsider C = CatStr(# F₁(),M,DM,CM,CC,I #) as strict Category ;
C is with_triple-like_morphisms

proof

let f be Morphism of C; :: according to CAT_5:def 1 :: thesis:
f in M ;
then consider a, b being Element of F₁(), g being Element of F₂() such that
A80: f = [[a,b],g] and
P₁[a,b,g] ;
take g ; :: thesis:
A81: dom f = f `11 by A10
.= a by A80, MCART_1:85 ;
cod f = f `12 by A11
.= b by A80, MCART_1:85 ;
hence f = [[(dom f),(cod f)],g] by A80, A81; :: thesis:

end;

then reconsider C = C as strict with_triple-like_morphisms Category ;
take C ; :: thesis:
thus the carrier of C = F₁() ; :: thesis:

hereby :: thesis:

let a, b be Element of F₁(); :: thesis:
let f be Element of F₂(); :: thesis:
assume P₁[a,b,f] ; :: thesis:
then [[a,b],f] in M ;
hence [[a,b],f] is Morphism of C ; :: thesis:

end;

hereby :: thesis:

let m be Morphism of C; :: thesis:
m in M ;
hence ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ; :: thesis:

end;

let m1, m2 be Morphism of C; :: thesis:
let a1, a2, a3 be Element of F₁(); :: thesis:
let f1, f2 be Element of F₂(); :: thesis:
assume that
A82: m1 = [[a1,a2],f1] and
A83: m2 = [[a2,a3],f2] ; :: thesis:
A84: m1 `11 = a1 by A82, MCART_1:85;
A85: m1 `12 = a2 by A82, MCART_1:85;
A86: m2 `11 = a2 by A83, MCART_1:85;
A87: m2 `12 = a3 by A83, MCART_1:85;
A88: [m2,m1] in dom CC by A25, A85, A86;
hence m2 * m1 = CC . (m2,m1) by CAT_1:def 1
.= [[a1,a3],F₃((m2 `2),(m1 `2))] by A26, A84, A87, A88
.= [[a1,a3],F₃(f2,(m1 `2))] by A83, MCART_1:7
.= [[a1,a3],F₃(f2,f1)] by A82, MCART_1:7 ;
:: thesis: