deffunc H₁( Element of Funcs (Carr P), Element of Funcs (Carr P)) -> set = $1 * $2;
defpred S₁[ Element of P, Element of P, Element of Funcs (Carr P)] means $3 in MonFuncs ($1,$2);

A6: now :: thesis: 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 ) ) ) )

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 ) ) ) )
thus 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 ) ) ) ) :: thesis: verum

proof

set f = id the carrier of a;
A7: id the carrier of a in MonFuncs (a,a) by Th7;
MonFuncs (a,a) c= Funcs (Carr P) by Th10;
then reconsider f = id the carrier of a as Element of Funcs (Carr P) by A7;

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 ) )
A8: ( 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 A8; :: thesis: verum

end;

hence 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 ) ) ) ) by A7; :: thesis: verum

end;

end;

thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = 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 C1 ) & ( for m being Morphism of C1 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 C1
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)] ) & the carrier of C2 = 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 C2 ) & ( for m being Morphism of C2 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 C2
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)] ) holds
C1 = C2 from CAT_5:sch 2(A6); :: thesis: verum