let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being covariant Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
let F1, F2 be covariant Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t ) )
assume A1: F1 is_transformable_to F2 ; :: thesis: for t being transformation of F1,F2 holds
( (idt F2) `*` t = t & t `*` (idt F1) = t )
let t be transformation of F1,F2; :: thesis: ( (idt F2) `*` t = t & t `*` (idt F1) = t )

now

let a be object of A; :: thesis: ((idt F2) `*` t) ! a = t ! a
A2: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F2 . a)^> <> {} ) by A1, Def1;
thus ((idt F2) `*` t) ! a = ((idt F2) ! a) * (t ! a) by A1, Def5
.= (idm (F2 . a)) * (t ! a) by Th6
.= t ! a by A2, ALTCAT_1:24 ; :: thesis: verum

end;

hence (idt F2) `*` t = t by A1, Th5; :: thesis: t `*` (idt F1) = t

now

let a be object of A; :: thesis: (t `*` (idt F1)) ! a = t ! a
A3: ( <^(F1 . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, Def1;
thus (t `*` (idt F1)) ! a = (t ! a) * ((idt F1) ! a) by A1, Def5
.= (t ! a) * (idm (F1 . a)) by Th6
.= t ! a by A3, ALTCAT_1:def 19 ; :: thesis: verum

end;

hence t `*` (idt F1) = t by A1, Th5; :: thesis: verum