let A be Category; :: thesis: ex F, G being Functor of A,A st
( G * F ~= id A & F * G ~= id A )
take id A ; :: 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