set F = the Functor of A,B;
take
{[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]}
; for x being set st x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
let x be set ; ( x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} implies ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
assume A1:
x in {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]}
; ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
take
the Functor of A,B
; ex F2 being Functor of A,B ex t being natural_transformation of the Functor of A,B,F2 st
( x = [[ the Functor of A,B,F2],t] & the Functor of A,B is_naturally_transformable_to F2 )
take
the Functor of A,B
; ex t being natural_transformation of the Functor of A,B, the Functor of A,B st
( x = [[ the Functor of A,B, the Functor of A,B],t] & the Functor of A,B is_naturally_transformable_to the Functor of A,B )
take
id the Functor of A,B
; ( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B )
thus
( x = [[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)] & the Functor of A,B is_naturally_transformable_to the Functor of A,B )
by A1, TARSKI:def 1; verum