set F = the Functor of A,B;
take {[[ the Functor of A,B, the Functor of A,B],(id the Functor of A,B)]} ; :: thesis: 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 ; :: thesis: ( 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)]} ; :: 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 the Functor of A,B ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum