let A, B be category; :: thesis: for F1, F2 being covariant Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being Object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
let F1, F2 be covariant Functor of A,B; :: thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being Object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
let t be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ( for a being Object of A holds t ! a is iso ) implies ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) ) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 and
A3: for a being Object of A holds t ! a is iso ; :: thesis: ( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
defpred S₁[ object , object ] means ex a being Object of A st
( a = $1 & $2 = (t ! a) " );
set I = the carrier of A;
A4: for i being object st i in the carrier of A holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in the carrier of A implies ex j being object st S₁[i,j] )
assume i in the carrier of A ; :: thesis: ex j being object st S₁[i,j]
then reconsider o = i as Object of A ;
take (t ! o) " ; :: thesis: S₁[i,(t ! o) " ]
thus S₁[i,(t ! o) " ] ; :: thesis: verum

end;

consider f being ManySortedSet of the carrier of A such that
A5: for i being object st i in the carrier of A holds
S₁[i,f . i] from PBOOLE:sch 3(A4);
f is transformation of F2,F1

proof

thus F2 is_transformable_to F1 by A2; :: according to FUNCTOR2:def 2 :: thesis: for b₁ being M3( the carrier of A) holds f . b₁ is M3(<^(F2 . b₁),(F1 . b₁)^>)
let a be Object of A; :: thesis: f . a is M3(<^(F2 . a),(F1 . a)^>)
ex b being Object of A st
( b = a & f . a = (t ! b) " ) by A5;
hence f . a is M3(<^(F2 . a),(F1 . a)^>) ; :: thesis: verum

end;

then reconsider f = f as transformation of F2,F1 ;
A6: F1 is_transformable_to F2 by A1;

A7: now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a)

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a) )
assume A8: <^a,b^> <> {} ; :: thesis: for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A9: <^(F1 . a),(F1 . b)^> <> {} by A8, FUNCTOR0:def 18;
let g be Morphism of a,b; :: thesis: (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A10: ex bb being Object of A st
( bb = b & f . b = (t ! bb) " ) by A5;
A11: t ! b is iso by A3;
A12: <^(F2 . a),(F1 . a)^> <> {} by A2;
A13: <^(F1 . a),(F2 . a)^> <> {} by A6;
A14: ex aa being Object of A st
( aa = a & f . a = (t ! aa) " ) by A5;
then reconsider fa = f . a as Morphism of (F2 . a),(F1 . a) ;
A15: t ! a is iso by A3;
A16: <^(F1 . b),(F2 . b)^> <> {} by A6;
A17: <^(F2 . b),(F1 . b)^> <> {} by A2;
A18: <^(F2 . a),(F2 . b)^> <> {} by A8, FUNCTOR0:def 18;
then A19: <^(F2 . a),(F1 . b)^> <> {} by A17, ALTCAT_1:def 2;
hence (f ! b) * (F2 . g) = ((f ! b) * (F2 . g)) * (idm (F2 . a)) by ALTCAT_1:def 17
.= ((f ! b) * (F2 . g)) * ((t ! a) * fa) by A14, A15, ALTCAT_3:def 5
.= ((f ! b) * (F2 . g)) * ((t ! a) * (f ! a)) by A2, FUNCTOR2:def 4
.= (((f ! b) * (F2 . g)) * (t ! a)) * (f ! a) by A13, A12, A19, ALTCAT_1:21
.= ((f ! b) * ((F2 . g) * (t ! a))) * (f ! a) by A13, A17, A18, ALTCAT_1:21
.= ((f ! b) * ((t ! b) * (F1 . g))) * (f ! a) by A1, A8, FUNCTOR2:def 7
.= (((f ! b) * (t ! b)) * (F1 . g)) * (f ! a) by A17, A16, A9, ALTCAT_1:21
.= ((((t ! b) ") * (t ! b)) * (F1 . g)) * (f ! a) by A2, A10, FUNCTOR2:def 4
.= ((idm (F1 . b)) * (F1 . g)) * (f ! a) by A11, ALTCAT_3:def 5
.= (F1 . g) * (f ! a) by A9, ALTCAT_1:20 ;
:: thesis: verum

end;

hence F2 is_naturally_transformable_to F1 by A2; :: thesis: ex f being natural_transformation of F2,F1 st
for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso )
F2 is_naturally_transformable_to F1 by A2, A7;
then reconsider f = f as natural_transformation of F2,F1 by A7, FUNCTOR2:def 7;
take f ; :: thesis: for a being Object of A holds
( f . a = (t ! a) " & f ! a is iso )
let a be Object of A; :: thesis: ( f . a = (t ! a) " & f ! a is iso )
consider b being Object of A such that
A20: b = a and
A21: f . a = (t ! b) " by A5;
thus f . a = (t ! a) " by A20, A21; :: thesis: f ! a is iso
A22: <^(F1 . a),(F2 . a)^> <> {} by A6;
A23: <^(F2 . a),(F1 . a)^> <> {} by A2;
f ! a = (t ! b) " by A2, A21, FUNCTOR2:def 4;
hence f ! a is iso by A3, A20, A22, A23, ALTCAT_4:3; :: thesis: verum