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 } ;
set a = the Element of X;
id the Element of X in Y by A2;
then id the Element of X 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

let x be object ; :: according to FUNCT_1:def 13 :: 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 that
A4: S₁[a,b,f] and
A5: S₁[b,c,g] ; :: thesis:
reconsider f = f as Functor of a,b by A4;
reconsider g = g as Functor of b,c by A5;
A6: f in B ;
A7: g in B ;
A8: ex b being Element of Y st
( f = b & b is Function ) by A6;
ex b being Element of Y st
( g = b & b is Function ) by A7;
then g * f in Y by A1, A8;
hence ( H₁(g,f) in B & S₁[a,c,H₁(g,f)] ) ; :: thesis:

end;

A9: 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:17; :: thesis:
assume S₁[b,a,g] ; :: thesis:
then reconsider G = g as Functor of b,a ;
(id a) * G = G by FUNCT_2:17;
hence H₁(f,g) = g ; :: thesis:

end;

A10: 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:36;
consider C being strict with_triple-like_morphisms Category such that
A11: ( 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, A9, A10);
C is Categorial

proof

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

hereby :: thesis:

let a be Object of C; :: thesis:
let D be Category; :: thesis:
assume A12: a = D ; :: thesis:
then id D in Y by A2, A11;
then id D in B ;
then reconsider f = id D as Element of B ;
reconsider x = a as Element of A by A11;
reconsider F = [[x,x],f] as Morphism of C by A11, A12;
consider b, c being Element of A, g being Element of B such that
A13: id a = [[b,c],g] and
A14: S₁[b,c,g] by A11;
A15: dom (id a) = (id a) `11 by Th2;
A16: (id a) `11 = b by A13, MCART_1:85;
cod F = F `12 by Th2
.= x by MCART_1:85 ;
then F = (id a) (*) F by CAT_1:21
.= [[x,c],(g * (id the carrier' of D))] by A11, A13, A15, A16
.= [[x,c],g] by A12, A14, A15, A16, FUNCT_2:17 ;
hence id a = [[D,D],(id D)] by A12, A13, A15, MCART_1:85; :: 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
A17: m = [[a,b],f] and
A18: S₁[a,b,f] by A11;
A19: dom m = m `11 by Th2;
A20: cod m = m `12 by Th2;
A21: dom m = a by A17, A19, MCART_1:85;
cod m = b by A17, A20, MCART_1:85;
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 A17, A18, A21; :: thesis:

end;

let m1, m2 be Morphism of C; :: thesis:
consider a1, b1 being Element of A, f1 being Element of B such that
A22: m1 = [[a1,b1],f1] and
S₁[a1,b1,f1] by A11;
consider a2, b2 being Element of A, f2 being Element of B such that
A23: m2 = [[a2,b2],f2] and
S₁[a2,b2,f2] by A11;
let A, B, C be Category; :: thesis:
let F be Functor of A,B; :: thesis:
let G be Functor of B,C; :: thesis:
assume that
A24: m1 = [[A,B],F] and
A25: m2 = [[B,C],G] ; :: thesis:
A26: [A,B] = [a1,b1] by A22, A24, XTUPLE_0:1;
A27: [B,C] = [a2,b2] by A23, A25, XTUPLE_0:1;
A28: f1 = F by A22, A24, XTUPLE_0:1;
A29: f2 = G by A23, A25, XTUPLE_0:1;
A30: A = a1 by A26, XTUPLE_0:1;
A31: B = b1 by A26, XTUPLE_0:1;
C = b2 by A27, XTUPLE_0:1;
hence m2 (*) m1 = [[A,C],(G * F)] by A11, A22, A25, A28, A29, A30, A31; :: thesis:

end;

then reconsider C = C as strict Categorial Category ;
take C ; :: thesis:
thus the carrier of C = X by A11; :: thesis:
let A9, B9 be Element of X; :: thesis:
let F be Functor of A9,B9; :: thesis:

hereby :: thesis:

assume [[A9,B9],F] is Morphism of C ; :: thesis:
then reconsider m = [[A9,B9],F] as Morphism of C ;
consider a, b being Element of A, f being Element of B such that
A32: m = [[a,b],f] and
S₁[a,b,f] by A11;
m `2 = f by A32;
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 [[A9,B9],F] is Morphism of C by A11; :: thesis: