deffunc H₁( Function, Function) -> set = $1 * $2;
defpred S₁[ Element of P, Element of P, set ] means $3 in MonFuncs ($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 ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; :: thesis: ( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] )
then A2: g * f in MonFuncs (a,c) by Th6;
MonFuncs (a,c) c= Funcs (Carr P) by Th10;
hence ( H₁(g,f) in Funcs (Carr P) & S₁[a,c,H₁(g,f)] ) by A2; :: thesis: verum

end;

A3: 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;
( MonFuncs (a,a) c= Funcs (Carr P) & id the carrier of a in MonFuncs (a,a) ) by Th7, Th10;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) ;
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 :: thesis: for b being Element of P
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 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 ) )
A4: ( g in MonFuncs (b,a) implies f * g = g )

proof

assume g in MonFuncs (b,a) ; :: thesis: f * g = g
then ex g9 being Function of b,a st
( g9 = g & g9 in Funcs ( the carrier of b, the carrier of a) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of b, the carrier of a ;
rng g c= the carrier of a ;
hence f * g = g by RELAT_1:53; :: thesis: verum

end;

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

proof

assume g in MonFuncs (a,b) ; :: thesis: g * f = g
then ex g9 being Function of a,b st
( g9 = g & g9 in Funcs ( the carrier of a, the carrier of b) & g9 is monotone ) by Def6;
then reconsider g = g as Function of the carrier of a, the carrier of b ;
dom g = the carrier of a by FUNCT_2:def 1;
hence g * f = g by RELAT_1:51; :: thesis: verum

end;

hence ( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) ) by A4; :: thesis: verum

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;

A5: 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:36;
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, A3, A5);
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