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_{1}[ 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_{1}[i,j]

A5: for i being object st i in the carrier of A holds

S_{1}[i,f . i]
from PBOOLE:sch 3(A4);

f is transformation of F2,F1

A6: F1 is_transformable_to F2 by A1;

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

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

( 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

proof

consider f being ManySortedSet of the carrier of A such that
let i be object ; :: thesis: ( i in the carrier of A implies ex j being object st S_{1}[i,j] )

assume i in the carrier of A ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider o = i as Object of A ;

take (t ! o) " ; :: thesis: S_{1}[i,(t ! o) " ]

thus S_{1}[i,(t ! o) " ]
; :: thesis: verum

end;assume i in the carrier of A ; :: thesis: ex j being object st S

then reconsider o = i as Object of A ;

take (t ! o) " ; :: thesis: S

thus S

A5: for i being object st i in the carrier of A holds

S

f is transformation of F2,F1

proof

then reconsider f = f as transformation of F2,F1 ;
thus
F2 is_transformable_to F1
by A2; :: according to FUNCTOR2:def 2 :: thesis: for b_{1} being M3( the carrier of A) holds f . b_{1} is M3(<^(F2 . b_{1}),(F1 . b_{1})^>)

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;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

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)

hence
F2 is_naturally_transformable_to F1
by A2; :: thesis: ex f being natural_transformation of F2,F1 st 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;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

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