let B, A 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 ) )
set I = the carrier of A;
defpred S1[ set , set ] means ex a being object of A st
( a = $1 & $2 = (t ! a) " );
A4: for i being set st i in the carrier of A holds
ex j being set st S1[i,j]
proof
let i be set ; :: thesis: ( i in the carrier of A implies ex j being set st S1[i,j] )
assume i in the carrier of A ; :: thesis: ex j being set st S1[i,j]
then reconsider o = i as object of A ;
take (t ! o) " ; :: thesis: S1[i,(t ! o) " ]
thus S1[i,(t ! o) " ] ; :: thesis: verum
end;
consider f being ManySortedSet of such that
A5: for i being set st i in the carrier of A holds
S1[i,f . i] from PBOOLE:sch 3(A4);
 A6: F1 is_transformable_to F2 by A1, FUNCTOR2:def 6;
f is transformation of F2,F1
proof
thus F2 is_transformable_to F1 by A2; :: according to FUNCTOR2:def 2 :: thesis: for b1 being M2(the carrier of A) holds f . b1 is M2(<^(F2 . b1),(F1 . b1)^>)
let a be object of A; :: thesis: f . a is M2(<^(F2 . a),(F1 . a)^>)
consider b being object of A such that
A7: ( b = a & f . a = (t ! b) " ) by A5;
thus f . a is M2(<^(F2 . a),(F1 . a)^>) by A7; :: thesis: verum
end;
then reconsider f = f as transformation of F2,F1 ;
A8: now
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 A9: <^a,b^> <> {} ; :: thesis: for g being Morphism of a,b holds (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A10: 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) ;
A11: ex bb being object of A st
( bb = b & f . b = (t ! bb) " ) by A5;
A12: t ! a is iso by A3;
A13: t ! b is iso by A3;
let g be Morphism of a,b; :: thesis: (f ! b) * (F2 . g) = (F1 . g) * (f ! a)
A14: <^(F1 . a),(F2 . a)^> <> {} by A6, FUNCTOR2:def 1;
A15: <^(F2 . a),(F1 . a)^> <> {} by A2, FUNCTOR2:def 1;
A16: <^(F2 . b),(F1 . b)^> <> {} by A2, FUNCTOR2:def 1;
A17: <^(F2 . a),(F2 . b)^> <> {} by A9, FUNCTOR0:def 19;
then A18: <^(F2 . a),(F1 . b)^> <> {} by A16, ALTCAT_1:def 4;
A19: <^(F1 . b),(F2 . b)^> <> {} by A6, FUNCTOR2:def 1;
A20: <^(F1 . a),(F1 . b)^> <> {} by A9, FUNCTOR0:def 19;
thus (f ! b) * (F2 . g) = ((f ! b) * (F2 . g)) * (idm (F2 . a)) by A18, ALTCAT_1:def 19
.= ((f ! b) * (F2 . g)) * ((t ! a) * fa) by A10, A12, 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 A14, A15, A18, ALTCAT_1:25
.= ((f ! b) * ((F2 . g) * (t ! a))) * (f ! a) by A14, A16, A17, ALTCAT_1:25
.= ((f ! b) * ((t ! b) * (F1 . g))) * (f ! a) by A1, A9, FUNCTOR2:def 7
.= (((f ! b) * (t ! b)) * (F1 . g)) * (f ! a) by A16, A19, A20, ALTCAT_1:25
.= ((((t ! b) " ) * (t ! b)) * (F1 . g)) * (f ! a) by A2, A11, FUNCTOR2:def 4
.= ((idm (F1 . b)) * (F1 . g)) * (f ! a) by A13, ALTCAT_3:def 5
.= (F1 . g) * (f ! a) by A20, ALTCAT_1:24 ; :: thesis: verum
end;
A21: F2 is_naturally_transformable_to F1
proof
thus F2 is_transformable_to F1 by A2; :: according to FUNCTOR2:def 6 :: thesis: ex b1 being transformation of F2,F1 st
for b2, b3 being M2(the carrier of A) holds
( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * (F2 . b4) = (F1 . b4) * (b1 ! b2) )
thus ex b1 being transformation of F2,F1 st
for b2, b3 being M2(the carrier of A) holds
( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * (F2 . b4) = (F1 . b4) * (b1 ! b2) ) by A8; :: thesis: verum
end;
f is natural_transformation of F2,F1
proof
thus F2 is_naturally_transformable_to F1 by A21; :: according to FUNCTOR2:def 7 :: thesis: for b1, b2 being M2(the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds (f ! b2) * (F2 . b3) = (F1 . b3) * (f ! b1) )
thus for b1, b2 being M2(the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds (f ! b2) * (F2 . b3) = (F1 . b3) * (f ! b1) ) by A8; :: thesis: verum
end;
then reconsider f = f as natural_transformation of F2,F1 ;
thus F2 is_naturally_transformable_to F1 by A21; :: 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 )
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
A22: ( b = a & f . a = (t ! b) " ) by A5;
thus f . a = (t ! a) " by A22; :: thesis: f ! a is iso
A23: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F1 . a)^> <> {} ) by A2, A6, FUNCTOR2:def 1;
f ! a = (t ! b) " by A2, A22, FUNCTOR2:def 4;
hence f ! a is iso by A3, A22, A23, ALTCAT_4:3; :: thesis: verum