let A, B be non empty transitive with_units AltCatStr ; for F, G being covariant Functor of A,B
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let F, G be covariant Functor of A,B; for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let a, b be Object of A; ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) )
assume A1:
<^a,b^> <> {}
; for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
let f be Morphism of a,b; ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
A2:
<^a,a^> <> {}
by ALTCAT_2:def 7;
A3:
<^b,b^> <> {}
by ALTCAT_2:def 7;
thus ((idt F) ! b) * (F . f) =
(idm (F . b)) * (F . f)
by Th4
.=
(F . (idm b)) * (F . f)
by Th1
.=
F . ((idm b) * f)
by A1, A3, FUNCTOR0:def 23
.=
F . f
by A1, ALTCAT_1:20
.=
F . (f * (idm a))
by A1, ALTCAT_1:def 17
.=
(F . f) * (F . (idm a))
by A1, A2, FUNCTOR0:def 23
.=
(F . f) * (idm (F . a))
by Th1
.=
(F . f) * ((idt F) ! a)
by Th4
; verum