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;
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);
( 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) )
;
( 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;
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;
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 Th7, Th10;
then reconsider f =
id the
carrier of
a as
Element of
Funcs (Carr P) ;
take
f
;
( 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 ) ) ) )
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;
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)] ) )
; verum