defpred S₁[ Element of P, Element of P, set ] means $3 in MonFuncs $1,$2;
deffunc H₁( Function, Function) -> set = $1 * $2;
A1: for a, b, c being Element of P
for f, g being Element of Funcs (Carr P) st S₁[a,b,f] & S₁[b,c,g] holds
( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] )

proof

let a, b, c be Element of P; :: thesis: for f, g being Element of Funcs (Carr P) st S₁[a,b,f] & S₁[b,c,g] holds
( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] )
let f, g be Element of Funcs (Carr P); :: thesis: ( S₁[a,b,f] & S₁[b,c,g] implies ( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] ) )
assume A2: ( f in MonFuncs a,b & g in MonFuncs b,c ) ; :: thesis: ( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] )
A3: MonFuncs a,c c= Funcs (Carr P) by Th10;
g * f in MonFuncs a,c by A2, Th6;
hence ( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] ) by A3; :: thesis: verum

end;

A4: for a being Element of P ex f being Element of Funcs (Carr P) st
( S₁[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) 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 P; :: thesis: ex f being Element of Funcs (Carr P) st
( S₁[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S₁[a,b,g] implies H₁(g,f) = g ) & ( S₁[b,a,g] implies H₁(f,g) = g ) ) ) )
set f = id the carrier of a;
A5: MonFuncs a,a c= Funcs (Carr P) by Th10;
id the carrier of a in MonFuncs a,a by Th7;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) by A5;
take f ; :: thesis: ( S₁[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S₁[a,b,g] implies H₁(g,f) = g ) & ( S₁[b,a,g] implies H₁(f,g) = g ) ) ) )

now

let b be Element of P; :: thesis: for g being Element of Funcs (Carr P) holds
( ( g in MonFuncs a,b implies g * f = g ) & ( g in MonFuncs b,a implies f * g = g ) )
let g be Element of Funcs (Carr P); :: thesis: ( ( g in MonFuncs a,b implies g * f = g ) & ( g in MonFuncs b,a implies f * g = g ) )
thus ( ( g in MonFuncs a,b implies g * f = g ) & ( g in MonFuncs b,a implies f * g = g ) ) :: thesis: verum

proof

thus ( g in MonFuncs a,b implies g * f = g ) :: thesis: ( g in MonFuncs b,a implies f * g = g )

proof

assume g in MonFuncs a,b ; :: thesis: g * f = g
then consider g' being Function of a,b such that
A6: ( g' = g & g' in Funcs the carrier of a,the carrier of b & g' is monotone ) by Def6;
reconsider g = g as Function of the carrier of a,the carrier of b by A6;
dom g = the carrier of a by FUNCT_2:def 1;
hence g * f = g by RELAT_1:77; :: thesis: verum

end;

thus ( g in MonFuncs b,a implies f * g = g ) :: thesis: verum

proof

assume g in MonFuncs b,a ; :: thesis: f * g = g
then consider g' being Function of b,a such that
A7: ( g' = g & g' in Funcs the carrier of b,the carrier of a & g' is monotone ) by Def6;
reconsider g = g as Function of the carrier of b,the carrier of a by A7;
rng g c= the carrier of a ;
hence f * g = g by RELAT_1:79; :: thesis: verum

end;

end;

end;

hence ( S₁[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S₁[a,b,g] implies H₁(g,f) = g ) & ( S₁[b,a,g] implies H₁(f,g) = g ) ) ) ) by Th7; :: thesis: verum

end;

A8: for a, b, c, d being Element of P
for f, g, h being Element of Funcs (Carr P) 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;
ex C being strict with_triple-like_morphisms Category st
( the carrier of C = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) 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 P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & S₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],H₁(f2,f1)] ) ) from CAT_5:sch 1(A1, A4, A8);
hence ex b₁ being strict with_triple-like_morphisms Category st
( the carrier of b₁ = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs a,b holds
[[a,b],f] is Morphism of b₁ ) & ( for m being Morphism of b₁ ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs a,b ) ) & ( for m1, m2 being Morphism of b₁
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) ) ; :: thesis: verum