let A be non empty transitive with_units AltCatStr ; :: thesis: ex F being Functor of A,A st
( F is bijective & F is covariant )
take id A ; :: thesis: ( id A is bijective & id A is covariant )
thus ( id A is bijective & id A is covariant ) ; :: thesis: verum