per cases ( not Mor D is empty or Mor D is empty ) ;
suppose not Mor D is empty ; :: thesis: ex b1 being Functor of C,D st
( b1 is identity-preserving & b1 is multiplicative & b1 is antimultiplicative )
then reconsider D1 = D as non empty with_identities CategoryStr ;
set F = (Mor C) --> the Object of D;
reconsider F = (Mor C) --> the Object of D as Function of C,D ;
take F ; :: thesis: ( F is identity-preserving & F is multiplicative & F is antimultiplicative )
A1: for f being morphism of C st f is identity holds
F . f is identity
proof
let f be morphism of C; :: thesis: ( f is identity implies F . f is identity )
assume f is identity ; :: thesis: F . f is identity
F . f is Object of D1 by Def21;
hence F . f is identity by Th22; :: thesis: verum
end;
( ( for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) ) & ( for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) ) ) ;
hence ( F is identity-preserving & F is multiplicative & F is antimultiplicative ) by A1; :: thesis: verum
end;
suppose A2: Mor D is empty ; :: thesis: ex b1 being Functor of C,D st
( b1 is identity-preserving & b1 is multiplicative & b1 is antimultiplicative )
set F = the Function of C,D;
take the Function of C,D ; :: thesis: ( the Function of C,D is identity-preserving & the Function of C,D is multiplicative & the Function of C,D is antimultiplicative )
A3: for f being morphism of C st f is identity holds
the Function of C,D . f is identity
proof
let f be morphism of C; :: thesis: ( f is identity implies the Function of C,D . f is identity )
assume f is identity ; :: thesis: the Function of C,D . f is identity
D is empty by A2;
hence the Function of C,D . f is identity by Th10; :: thesis: verum
end;
( ( for f1, f2 being morphism of C st f1 |> f2 holds
( the Function of C,D . f1 |> the Function of C,D . f2 & the Function of C,D . (f1 (*) f2) = ( the Function of C,D . f1) (*) ( the Function of C,D . f2) ) ) & ( for f1, f2 being morphism of C st f1 |> f2 holds
( the Function of C,D . f2 |> the Function of C,D . f1 & the Function of C,D . (f1 (*) f2) = ( the Function of C,D . f2) (*) ( the Function of C,D . f1) ) ) ) ;
hence ( the Function of C,D is identity-preserving & the Function of C,D is multiplicative & the Function of C,D is antimultiplicative ) by A3; :: thesis: verum
end;
end;