deffunc H1( set , set , set , set , set ) -> set = F3($1,$2,$3,$4,$5);
A5:
for a, b, c being Element of F1()
for f, g being set st f in F2(a,b) & g in F2(b,c) holds
H1(a,b,c,f,g) in F2(a,c)
by A1;
consider C being non empty transitive strict AltCatStr such that
A6:
the carrier of C = F1()
and
A7:
for a, b being object of C holds <^a,b^> = F2(a,b)
and
A8:
for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H1(a,b,c,f,g)
from YELLOW18:sch 1(A5);
A9:
for a, b, c, d being object of C
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))
proof
let a,
b,
c,
d be
object of
C;
for f, g, h being set st f in <^a,b^> & g in <^b,c^> & h in <^c,d^> holds
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))let f,
g,
h be
set ;
( f in <^a,b^> & g in <^b,c^> & h in <^c,d^> implies H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h)) )
assume that A10:
f in <^a,b^>
and A11:
g in <^b,c^>
and A12:
h in <^c,d^>
;
H1(a,c,d,H1(a,b,c,f,g),h) = H1(a,b,d,f,H1(b,c,d,g,h))
A13:
<^a,b^> = F2(
a,
b)
by A7;
A14:
<^b,c^> = F2(
b,
c)
by A7;
<^c,d^> = F2(
c,
d)
by A7;
hence
H1(
a,
c,
d,
H1(
a,
b,
c,
f,
g),
h)
= H1(
a,
b,
d,
f,
H1(
b,
c,
d,
g,
h))
by A2, A6, A10, A11, A12, A13, A14;
verum
end;
A15:
for a being object of C ex f being set st
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g ) )
proof
let a be
object of
C;
ex f being set st
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g ) )
consider f being
set such that A16:
f in F2(
a,
a)
and A17:
for
b being
Element of
F1()
for
g being
set st
g in F2(
a,
b) holds
H1(
a,
a,
b,
f,
g)
= g
by A3, A6;
take
f
;
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g ) )
thus
f in <^a,a^>
by A7, A16;
for b being object of C
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g
let b be
object of
C;
for g being set st g in <^a,b^> holds
H1(a,a,b,f,g) = g
<^a,b^> = F2(
a,
b)
by A7;
hence
for
g being
set st
g in <^a,b^> holds
H1(
a,
a,
b,
f,
g)
= g
by A6, A17;
verum
end;
A18:
for a being object of C ex f being set st
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g ) )
proof
let a be
object of
C;
ex f being set st
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g ) )
consider f being
set such that A19:
f in F2(
a,
a)
and A20:
for
b being
Element of
F1()
for
g being
set st
g in F2(
b,
a) holds
H1(
b,
a,
a,
g,
f)
= g
by A4, A6;
take
f
;
( f in <^a,a^> & ( for b being object of C
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g ) )
thus
f in <^a,a^>
by A7, A19;
for b being object of C
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g
let b be
object of
C;
for g being set st g in <^b,a^> holds
H1(b,a,a,g,f) = g
<^b,a^> = F2(
b,
a)
by A7;
hence
for
g being
set st
g in <^b,a^> holds
H1(
b,
a,
a,
g,
f)
= g
by A6, A20;
verum
end;
A21:
C is associative
from YELLOW18:sch 2(A8, A9);
C is with_units
from YELLOW18:sch 3(A8, A15, A18);
hence
ex C being strict category st
( the carrier of C = F1() & ( for a, b being object of C holds <^a,b^> = F2(a,b) ) & ( for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
by A6, A7, A8, A21; verum