consider F being Functor of A,B;
take {[[F,F],(id F)]} ; :: thesis: for x being set st x in {[[F,F],(id F)]} 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 ; :: thesis: ( x in {[[F,F],(id F)]} 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 {[[F,F],(id F)]} ; :: thesis: 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 F ; :: thesis: ex F2 being Functor of A,B ex t being natural_transformation of F,F2 st
( x = [[F,F2],t] & F is_naturally_transformable_to F2 )
take F ; :: thesis: ex t being natural_transformation of F,F st
( x = [[F,F],t] & F is_naturally_transformable_to F )
take id F ; :: thesis: ( x = [[F,F],(id F)] & F is_naturally_transformable_to F )
thus ( x = [[F,F],(id F)] & F is_naturally_transformable_to F ) by A1, TARSKI:def 1; :: thesis: verum