deffunc H1( Function, Function) -> set = \$1 * \$2;
defpred S1[ 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 S1[a,b,f] & S1[b,c,g] holds
( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )
proof
let a, b, c be Element of P; :: thesis: for f, g being Element of Funcs (Carr P) st S1[a,b,f] & S1[b,c,g] holds
( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )

let f, g be Element of Funcs (Carr P); :: thesis: ( S1[a,b,f] & S1[b,c,g] implies ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) )
assume ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; :: thesis: ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] )
then A2: g * f in MonFuncs (a,c) by Th6;
MonFuncs (a,c) c= Funcs (Carr P) by Th10;
hence ( H1(g,f) in Funcs (Carr P) & S1[a,c,H1(g,f)] ) by A2; :: thesis: verum
end;
A3: for a being Element of P ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
proof
let a be Element of P; :: thesis: ex f being Element of Funcs (Carr P) st
( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(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 ;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) ;
take f ; :: thesis: ( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(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 ( S1[a,a,f] & ( for b being Element of P
for g being Element of Funcs (Carr P) holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(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 S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(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 S1[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] & S1[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],H1(f2,f1)] ) ) from CAT_5:sch 1(A1, A3, A5);
hence ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = 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 b1 ) & ( for m being Morphism of b1 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 b1
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