let X be non empty categorial set ; :: thesis:
let Y be non empty set ; :: thesis:
assume that
A1: for A, B, C being Element of X
for F being Functor of A,B
for G being Functor of B,C st F in Y & G in Y holds
G * F in Y and
A2: for A being Element of X holds id A in Y ; :: thesis:
set B = { b where b is Element of Y : b is Function } ;
consider a being Element of X;
id a in Y by A2;
then id a in { b where b is Element of Y : b is Function } ;
then reconsider B = { b where b is Element of Y : b is Function } as non empty set ;
B is functional

proof

let x be set ; :: according to FUNCT_1:def 19 :: thesis:
assume x in B ; :: thesis:
then ex b being Element of Y st
( x = b & b is Function ) ;
hence x is set ; :: thesis:

end;

then reconsider B = B as non empty functional set ;
reconsider A = X as non empty categorial set ;
defpred S₁[ Element of A, Element of A, set ] means $3 is Functor of $1,$2;
deffunc H₁( Function, Function) -> set = $1 * $2;
A3: for a, b, c being Element of A
for f, g being Element of B st S₁[a,b,f] & S₁[b,c,g] holds
( H₁(g,f) in B & S₁[a,c,H₁(g,f)] )

proof

let a, b, c be Element of A; :: thesis:
let f, g be Element of B; :: thesis:
assume A4: ( S₁[a,b,f] & S₁[b,c,g] ) ; :: thesis:
then reconsider f = f as Functor of a,b ;
reconsider g = g as Functor of b,c by A4;
( f in B & g in B ) ;
then ( ex b being Element of Y st
( f = b & b is Function ) & ex b being Element of Y st
( g = b & b is Function ) ) ;
then g * f in Y by A1;
hence ( H₁(g,f) in B & S₁[a,c,H₁(g,f)] ) ; :: thesis:

end;

A5: for a being Element of A ex f being Element of B st
( S₁[a,a,f] & ( for b being Element of A
for g being Element of B holds
( ( S₁[a,b,g] implies H₁(g,f) = g ) & ( S₁[b,a,g] implies H₁(f,g) = g ) ) ) )

proof

let a be Element of A; :: thesis:
reconsider f = id a as Element of Y by A2;
f in B ;
then reconsider f = f as Element of B ;
take f ; :: thesis:
thus S₁[a,a,f] ; :: thesis:
let b be Element of A; :: thesis:
let g be Element of B; :: thesis:
thus ( S₁[a,b,g] implies g * f = g ) by FUNCT_2:23; :: thesis:
assume S₁[b,a,g] ; :: thesis:
then reconsider G = g as Functor of b,a ;
(id a) * G = G by FUNCT_2:23;
hence H₁(f,g) = g ; :: thesis:

end;

A6: for a, b, c, d being Element of A
for f, g, h being Element of B st S₁[a,b,f] & S₁[b,c,g] & S₁[c,d,h] holds
H₁(h,H₁(g,f)) = H₁(H₁(h,g),f) by RELAT_1:55;
consider C being strict with_triple-like_morphisms Category such that
A7: ( the carrier of C = A & ( for a, b being Element of A
for f being Element of B st S₁[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of A ex f being Element of B st
( m = [[a,b],f] & S₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of A
for f1, f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],H₁(f2,f1)] ) ) from CAT_5:sch 1(A3, A5, A6);
C is Categorial

proof

thus the carrier of C is categorial by A7; :: according to CAT_5:def 6 :: thesis:

hereby :: thesis:

let a be Object of C; :: thesis:
let D be Category; :: thesis:
assume A8: a = D ; :: thesis:
then id D in Y by A2, A7;
then id D in B ;
then reconsider f = id D as Element of B ;
reconsider x = a as Element of A by A7;
reconsider F = [[x,x],f] as Morphism of C by A7, A8;
consider b, c being Element of A, g being Element of B such that
A9: ( id a = [[b,c],g] & S₁[b,c,g] ) by A7;
A10: ( dom (id a) = a & cod (id a) = a & dom (id a) = (id a) `11 & cod (id a) = (id a) `12 & (id a) `11 = b & (id a) `12 = c ) by A9, Th2, CAT_1:44, MCART_1:89;
cod F = F `12 by Th2
.= x by MCART_1:89 ;
then F = (id a) * F by CAT_1:46
.= [[x,c],(g * (id the carrier' of D))] by A7, A9, A10
.= [[x,c],g] by A8, A9, A10, FUNCT_2:23 ;
hence id a = [[D,D],(id D)] by A8, A9, A10; :: thesis:

end;

hereby :: thesis:

let m be Morphism of C; :: thesis:
consider a, b being Element of A, f being Element of B such that
A11: ( m = [[a,b],f] & S₁[a,b,f] ) by A7;
( dom m = m `11 & cod m = m `12 ) by Th2;
then ( dom m = a & cod m = b ) by A11, MCART_1:89;
hence for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] by A11; :: thesis:

end;

let m1, m2 be Morphism of C; :: thesis:
consider a1, b1 being Element of A, f1 being Element of B such that
A12: ( m1 = [[a1,b1],f1] & S₁[a1,b1,f1] ) by A7;
consider a2, b2 being Element of A, f2 being Element of B such that
A13: ( m2 = [[a2,b2],f2] & S₁[a2,b2,f2] ) by A7;
let A, B, C be Category; :: thesis:
let F be Functor of A,B; :: thesis:
let G be Functor of B,C; :: thesis:
assume ( m1 = [[A,B],F] & m2 = [[B,C],G] ) ; :: thesis:
then A14: ( [A,B] = [a1,b1] & [B,C] = [a2,b2] & f1 = F & f2 = G ) by A12, A13, ZFMISC_1:33;
then ( A = a1 & B = b1 & B = a2 & C = b2 ) by ZFMISC_1:33;
hence m2 * m1 = [[A,C],(G * F)] by A7, A12, A13, A14; :: thesis:

end;

then reconsider C = C as strict Categorial Category ;
take C ; :: thesis:
thus the carrier of C = X by A7; :: thesis:
let A', B' be Element of X; :: thesis:
let F be Functor of A',B'; :: thesis:

hereby :: thesis:

assume [[A',B'],F] is Morphism of C ; :: thesis:
then reconsider m = [[A',B'],F] as Morphism of C ;
consider a, b being Element of A, f being Element of B such that
A15: ( m = [[a,b],f] & S₁[a,b,f] ) by A7;
( m `2 = F & m `2 = f ) by A15, MCART_1:7;
then F in B ;
then ex b being Element of Y st
( F = b & b is Function ) ;
hence F in Y ; :: thesis:

end;

assume F in Y ; :: thesis:
then F in B ;
hence [[A',B'],F] is Morphism of C by A7; :: thesis: