let A be Category; :: thesis: id A is Equivalence of A,A
thus A is_equivalent_with A ; :: according to ISOCAT_1:def 11 :: thesis: ex G being Functor of A,A st
( G * (id A) ~= id A & (id A) * G ~= id A )
take id A ; :: thesis: ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A )
thus ( (id A) * (id A) ~= id A & (id A) * (id A) ~= id A ) by FUNCT_2:17; :: thesis: verum