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 7,
ALTCAT_1:def 16 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 8
.=
g
by A1, A4, A6, A7
;
verum
end;
let i be Element of the carrier of F1(); ALTCAT_1:def 6 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 8
.=
f
by A1, A8, A10, A11
; verum