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

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

( 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

then reconsider f = f as natural_equivalence of F2,F1 ;
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;let a be Object of A; :: thesis: f ! a is iso

thus f ! a is iso by A3; :: thesis: verum

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