set alt = F1();
set IT = the Comp of F1();
set I = the carrier of F1();
set G = the Arrows of F1();
hereby ALTCAT_1:def 9,
ALTCAT_1:def 18 the Comp of F1() is with_right_units
let j be
Element of the
carrier of
F1();
ex f being set st
( f in the Arrows of F1() . j,j & ( for i being Element of the carrier of F1()
for g being set st g in the Arrows of F1() . i,j holds
(the Comp of F1() . i,j,j) . f,g = g ) )reconsider j9 =
j as
object of
F1() ;
consider f being
set such that A4:
f in <^j9,j9^>
and A5:
for
b being
Element of
F1()
for
g being
set st
g in <^b,j9^> holds
F2(
b,
j9,
j9,
g,
f)
= g
by A3;
take f =
f;
( f in the Arrows of F1() . j,j & ( for i being Element of the carrier of F1()
for g being set st g in the Arrows of F1() . i,j holds
(the Comp of F1() . i,j,j) . f,g = g ) )thus
f in the
Arrows of
F1()
. j,
j
by A4;
for i being Element of the carrier of F1()
for g being set st g in the Arrows of F1() . i,j holds
(the Comp of F1() . i,j,j) . f,g = glet i be
Element of the
carrier of
F1();
for g being set st g in the Arrows of F1() . i,j holds
(the Comp of F1() . i,j,j) . f,g = glet g be
set ;
( g in the Arrows of F1() . i,j implies (the Comp of F1() . i,j,j) . f,g = g )assume A6:
g in the
Arrows of
F1()
. i,
j
;
(the Comp of F1() . i,j,j) . f,g = greconsider i9 =
i as
object of
F1() ;
the
Arrows of
F1()
. i,
j = <^i9,j9^>
;
then A7:
F2(
i,
j,
j,
g,
f)
= g
by A5, A6;
reconsider f9 =
f as
Morphism of
j9,
j9 by A4;
reconsider g9 =
g as
Morphism of
i9,
j9 by A6;
thus (the Comp of F1() . i,j,j) . f,
g =
f9 * g9
by A4, A6, ALTCAT_1:def 10
.=
g
by A1, A4, A6, A7
;
verum
end;
let i be Element of the carrier of F1(); ALTCAT_1:def 8 ex b1 being set st
( b1 in the Arrows of F1() . i,i & ( for b2 being Element of the carrier of F1()
for b3 being set holds
( not b3 in the Arrows of F1() . i,b2 or (the Comp of F1() . i,i,b2) . b3,b1 = b3 ) ) )
reconsider i9 = i as object of F1() ;
consider e being set such that
A8:
e in <^i9,i9^>
and
A9:
for b being Element of F1()
for g being set st g in <^i9,b^> holds
F2(i,i,b,e,g) = g
by A2;
take
e
; ( e in the Arrows of F1() . i,i & ( for b1 being Element of the carrier of F1()
for b2 being set holds
( not b2 in the Arrows of F1() . i,b1 or (the Comp of F1() . i,i,b1) . b2,e = b2 ) ) )
thus
e in the Arrows of F1() . i,i
by A8; for b1 being Element of the carrier of F1()
for b2 being set holds
( not b2 in the Arrows of F1() . i,b1 or (the Comp of F1() . i,i,b1) . b2,e = b2 )
reconsider e9 = e as Morphism of i9,i9 by A8;
let j be Element of the carrier of F1(); for b1 being set holds
( not b1 in the Arrows of F1() . i,j or (the Comp of F1() . i,i,j) . b1,e = b1 )
let f be set ; ( not f in the Arrows of F1() . i,j or (the Comp of F1() . i,i,j) . f,e = f )
assume A10:
f in the Arrows of F1() . i,j
; (the Comp of F1() . i,i,j) . f,e = f
reconsider j9 = j as object of F1() ;
the Arrows of F1() . i,j = <^i9,j9^>
;
then A11:
F2(i,i,j,e,f) = f
by A9, A10;
reconsider f9 = f as Morphism of i9,j9 by A10;
thus (the Comp of F1() . i,i,j) . f,e =
f9 * e9
by A8, A10, ALTCAT_1:def 10
.=
f
by A1, A8, A10, A11
; verum