set M = { [[a,b],f] where a, b is Element of F₁(), f is Element of F₂() : P₁[a,b,f] } ;
consider a0 being Element of F₁();
consider f0 being Element of F₂() such that
A4: ( P₁[a0,a0,f0] & ( for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[a0,b,g] implies F₃(g,f0) = g ) & ( P₁[b,a0,g] implies F₃(f0,g) = g ) ) ) ) by A2;
A5: [[a0,a0],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₂():]

proof

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] & P₁[a,b,f] ) ;
( m `11 = a & m `12 = b & m `2 = f ) by A7, MCART_1:7, MCART_1:89;
hence ( m = [[(m `11 ),(m `12 )],(m `2 )] & P₁[m `11 ,m `12 ,m `2 ] ) by A7; :: thesis:

end;

deffunc H₁( Element of M) -> Element of F₁() = $1 `11 ;
consider DM being Function of M,F₁() such that
A8: 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
A9: 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 );

A10: now

let x, y be set ; :: thesis:
assume A11: S₁[x,y] ; :: thesis:
then consider ax, bx being Element of F₁(), fx being Element of F₂() such that
A12: ( x = [[ax,bx],fx] & P₁[ax,bx,fx] ) ;
consider ay, b2 being Element of F₁(), fy being Element of F₂() such that
A13: ( y = [[ay,b2],fy] & P₁[ay,b2,fy] ) by A11;
A14: ( x `11 = ax & x `12 = bx & y `11 = ay & y `12 = b2 & x `2 = fx & y `2 = fy ) by A12, A13, MCART_1:7, MCART_1:89;
then ( F₃(fx,fy) in F₂() & P₁[ay,bx,F₃(fx,fy)] ) by A1, A11, A12, A13;
hence H₃(x,y) in M by A14; :: thesis:

end;

consider CC being PartFunc of [:M,M:],M such that
A15: for x, y being set holds
( [x,y] in dom CC iff ( x in M & y in M & S₁[x,y] ) ) and
A16: for x, y being set st [x,y] in dom CC holds
CC . x,y = H₃(x,y) from BINOP_1:sch 6(A10);
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 ) ) ) );

A17: now

let a be Element of F₁(); :: thesis:
consider f being Element of F₂() such that
A18: ( P₁[a,a,f] & ( 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 A18;
then reconsider y = [[a,a],f] as Element of M ;
take y = y; :: thesis:
thus S₂[a,y] by A18; :: thesis:

end;

consider I being Function of F₁(),M such that
A19: for o being Element of F₁() holds S₂[o,I . o] from FUNCT_2:sch 3(A17);
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 8 :: thesis:

let f, g be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
( ( [g,f] in dom CC implies ( g in M & f in M & g `11 = f `12 & g in M & f in M ) ) & ( g in M & f in M & g `11 = f `12 & g in M & f in M implies [g,f] in dom CC ) & DM . g = g `11 & CM . f = f `12 ) by A8, A9, A15;
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 ) ; :: thesis:

end;

hereby :: thesis:

let f, g be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
A20: ( the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `11 & the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `11 & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `12 & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `12 ) by A8, A9;
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 [g,f] in dom CC by A15, A20;
then ( CC . g,f = [[(f `11 ),(g `12 )],F₃((g `2 ),(f `2 ))] & CC . g,f in rng CC & rng CC c= M ) by A16, FUNCT_1:def 5;
then ( (CC . [g,f]) `11 = f `11 & (CC . [g,f]) `12 = g `12 & CC . [g,f] in M ) by MCART_1:89;
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 A8, A9, A20; :: thesis:

end;

hereby :: thesis:

let f, g, h be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
A21: ( the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `11 & the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `11 & the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . h = h `11 & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . h = h `12 & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f = f `12 & the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g = g `12 ) by A8, A9;
assume A22: ( the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . h = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . g & the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . g = the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f ) ; :: thesis:
then A23: ( [g,f] in dom CC & [h,g] in dom CC ) by A15, A21;
then ( CC . [g,f] in rng CC & CC . [h,g] in rng CC & rng CC c= M ) by FUNCT_1:def 5;
then reconsider gf = CC . g,f, hg = CC . h,g as Element of M ;
A24: ( gf = [[(f `11 ),(g `12 )],F₃((g `2 ),(f `2 ))] & hg = [[(g `11 ),(h `12 )],F₃((h `2 ),(g `2 ))] ) by A16, A23;
A25: ( DM . gf = gf `11 & DM . hg = hg `11 & CM . gf = gf `12 & CM . hg = hg `12 ) by A8, A9;
then A26: ( DM . gf = f `11 & DM . hg = g `11 & CM . gf = g `12 & CM . hg = h `12 ) by A24, MCART_1:89;
then A27: ( [h,gf] in dom CC & [hg,f] in dom CC ) by A15, A21, A22, A25;
reconsider f' = f, g' = g, h' = h as Element of M ;
A28: ( P₁[f' `11 ,f' `12 ,f' `2 ] & P₁[g' `11 ,g' `12 ,g' `2 ] & P₁[h' `11 ,h' `12 ,h' `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 A16, A25, A26, A27
.= [[(f `11 ),(h `12 )],F₃((h' `2 ),F₃((g' `2 ),(f' `2 )))] by A24, MCART_1:7
.= [[(f `11 ),(h `12 )],F₃(F₃((h' `2 ),(g' `2 )),(f' `2 ))] by A3, A21, A22, A28
.= [[(f `11 ),(h `12 )],F₃((hg `2 ),(f `2 ))] by A24, 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 A16, A25, A26, A27 ; :: thesis:

end;

let b be Object of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
consider f being Element of F₂() such that
A29: ( I . b = [[b,b],f] & P₁[b,b,f] & ( 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 A19;
reconsider b' = b as Element of F₁() ;
reconsider Ib = I . b' 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 A8
.= b by A29, MCART_1:89 ; :: 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 A9
.= b by A29, MCART_1:89 ; :: thesis:

hereby :: thesis:

let f' be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
reconsider g = f' as Element of M ;
assume the Target of CatStr(# F₁(),M,DM,CM,CC,I #) . f' = b ; :: thesis:
then A30: ( g `12 = b & Ib `11 = b ) by A9, A29, MCART_1:89;
then ( P₁[g `11 ,b,g `2 ] & [Ib,g] in dom CC & Ib `12 = b & Ib `2 = f ) by A6, A15, A29, MCART_1:7, MCART_1:89;
then ( F₃(f,(g `2 )) = g `2 & CC . Ib,g = [[(g `11 ),b],F₃(f,(g `2 ))] ) by A16, A29;
hence the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . (the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b),f' = f' by A6, A30; :: thesis:

end;

let f' be Morphism of CatStr(# F₁(),M,DM,CM,CC,I #); :: thesis:
reconsider g = f' as Element of M ;
assume the Source of CatStr(# F₁(),M,DM,CM,CC,I #) . f' = b ; :: thesis:
then A31: ( g `11 = b & Ib `12 = b ) by A8, A29, MCART_1:89;
then ( P₁[b,g `12 ,g `2 ] & [g,Ib] in dom CC & Ib `11 = b & Ib `2 = f ) by A6, A15, A29, MCART_1:7, MCART_1:89;
then ( F₃((g `2 ),f) = g `2 & CC . g,Ib = [[b,(g `12 )],F₃((g `2 ),f)] ) by A16, A29;
hence the Comp of CatStr(# F₁(),M,DM,CM,CC,I #) . f',(the Id of CatStr(# F₁(),M,DM,CM,CC,I #) . b) = f' by A6, A31; :: 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
A32: ( f = [[a,b],g] & P₁[a,b,g] ) ;
take g ; :: thesis:
A33: dom f = f `11 by A8
.= a by A32, MCART_1:89 ;
cod f = f `12 by A9
.= b by A32, MCART_1:89 ;
hence f = [[(dom f),(cod f)],g] by A32, A33; :: 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 A34: ( m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] ) ; :: thesis:
then A35: ( m1 `11 = a1 & m1 `12 = a2 & m2 `11 = a2 & m2 `12 = a3 ) by MCART_1:89;
then A36: [m2,m1] in dom CC by A15;
hence m2 * m1 = CC . m2,m1 by CAT_1:def 4
.= [[a1,a3],F₃((m2 `2 ),(m1 `2 ))] by A16, A35, A36
.= [[a1,a3],F₃(f2,(m1 `2 ))] by A34, MCART_1:7
.= [[a1,a3],F₃(f2,f1)] by A34, MCART_1:7 ;
:: thesis: