let A be category; :: thesis: A, Concretized A are_isomorphic
take Concretization A ; :: according to FUNCTOR0:def 39 :: thesis: ( Concretization A is bijective & Concretization A is covariant )
thus ( Concretization A is bijective & Concretization A is covariant ) ; :: thesis: verum