deffunc H_{1}( Function, Function) -> set = $1 * $2;

defpred S_{1}[ 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_{1}[a,b,f] & S_{1}[b,c,g] holds

( H_{1}(g,f) in Funcs (Carr P) & S_{1}[a,c,H_{1}(g,f)] )

( S_{1}[a,a,f] & ( for b being Element of P

for g being Element of Funcs (Carr P) holds

( ( S_{1}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{1}[b,a,g] implies H_{1}(f,g) = g ) ) ) )

for f, g, h being Element of Funcs (Carr P) st S_{1}[a,b,f] & S_{1}[b,c,g] & S_{1}[c,d,h] holds

H_{1}(h,H_{1}(g,f)) = H_{1}(H_{1}(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_{1}[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_{1}[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_{1}(f2,f1)] ) )
from CAT_5:sch 1(A1, A3, A5);

hence ex b_{1} being strict with_triple-like_morphisms Category st

( the carrier of b_{1} = 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_{1} ) & ( for m being Morphism of b_{1} 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_{1}

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

defpred S

A1: for a, b, c being Element of P

for f, g being Element of Funcs (Carr P) st S

( H

proof

A3:
for a being Element of P ex f being Element of Funcs (Carr P) st
let a, b, c be Element of P; :: thesis: for f, g being Element of Funcs (Carr P) st S_{1}[a,b,f] & S_{1}[b,c,g] holds

( H_{1}(g,f) in Funcs (Carr P) & S_{1}[a,c,H_{1}(g,f)] )

let f, g be Element of Funcs (Carr P); :: thesis: ( S_{1}[a,b,f] & S_{1}[b,c,g] implies ( H_{1}(g,f) in Funcs (Carr P) & S_{1}[a,c,H_{1}(g,f)] ) )

assume ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; :: thesis: ( H_{1}(g,f) in Funcs (Carr P) & S_{1}[a,c,H_{1}(g,f)] )

then A2: g * f in MonFuncs (a,c) by Th6;

MonFuncs (a,c) c= Funcs (Carr P) by Th10;

hence ( H_{1}(g,f) in Funcs (Carr P) & S_{1}[a,c,H_{1}(g,f)] )
by A2; :: thesis: verum

end;( H

let f, g be Element of Funcs (Carr P); :: thesis: ( S

assume ( f in MonFuncs (a,b) & g in MonFuncs (b,c) ) ; :: thesis: ( H

then A2: g * f in MonFuncs (a,c) by Th6;

MonFuncs (a,c) c= Funcs (Carr P) by Th10;

hence ( H

( S

for g being Element of Funcs (Carr P) holds

( ( S

proof

A5:
for a, b, c, d being Element of P
let a be Element of P; :: thesis: ex f being Element of Funcs (Carr P) st

( S_{1}[a,a,f] & ( for b being Element of P

for g being Element of Funcs (Carr P) holds

( ( S_{1}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{1}[b,a,g] implies H_{1}(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_{1}[a,a,f] & ( for b being Element of P

for g being Element of Funcs (Carr P) holds

( ( S_{1}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{1}[b,a,g] implies H_{1}(f,g) = g ) ) ) )

_{1}[a,a,f] & ( for b being Element of P

for g being Element of Funcs (Carr P) holds

( ( S_{1}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{1}[b,a,g] implies H_{1}(f,g) = g ) ) ) )
by Th7; :: thesis: verum

end;( S

for g being Element of Funcs (Carr P) holds

( ( S

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

for g being Element of Funcs (Carr P) holds

( ( S

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 ) )

hence
( Sfor 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 )

end;( ( 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

( g in MonFuncs (a,b) implies g * f = g )
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;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

proof

hence
( ( g in MonFuncs (a,b) implies g * f = g ) & ( g in MonFuncs (b,a) implies f * g = g ) )
by A4; :: thesis: verum
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;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

for g being Element of Funcs (Carr P) holds

( ( S

for f, g, h being Element of Funcs (Carr P) st S

H

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] 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

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

hence ex b

( the carrier of b

for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds

[[a,b],f] is Morphism of b

( 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