A2: for a being Object of A holds e ! a is iso by A1, Def5;
( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 ) by A1;
then consider f being natural_transformation of F2,F1 such that
A3: for a being Object of A holds
( f . a = (e ! a) " & f ! a is iso ) by A2, Th32;
f is natural_equivalence of F2,F1
proof
thus F2,F1 are_naturally_equivalent by A1; :: according to FUNCTOR3:def 5 :: thesis: for a being Object of A holds f ! a is iso
let a be Object of A; :: thesis: f ! a is iso
thus f ! a is iso by A3; :: thesis: verum
end;
then reconsider f = f as natural_equivalence of F2,F1 ;
take f ; :: thesis: for a being Object of A holds f . a = (e ! a) "
let a be Object of A; :: thesis: f . a = (e ! a) "
thus f . a = (e ! a) " by A3; :: thesis: verum