let A, B be non empty transitive with_units AltCatStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( <^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^> <> {} ; :: thesis: 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; :: thesis: ((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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: ( <^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^> <> {} ; :: thesis: 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; :: thesis: ((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 ; :: thesis: verum