set C = the non empty category;
set D = the empty category;
set F = the identity-preserving Functor of the non empty category, the empty category;
take the non empty category ; :: thesis: ex D being category ex F being Functor of the non empty category,D st
( not F is multiplicative & F is identity-preserving )
take the empty category ; :: thesis: ex F being Functor of the non empty category, the empty category st
( not F is multiplicative & F is identity-preserving )
take the identity-preserving Functor of the non empty category, the empty category ; :: thesis: ( not the identity-preserving Functor of the non empty category, the empty category is multiplicative & the identity-preserving Functor of the non empty category, the empty category is identity-preserving )
thus ( not the identity-preserving Functor of the non empty category, the empty category is multiplicative & the identity-preserving Functor of the non empty category, the empty category is identity-preserving ) by Th29; :: thesis: verum