per cases ( not C is empty or C is empty ) ;
suppose A1: not C is empty ; :: thesis: ex b1 being Functor of C,D st
( b1 is identity-preserving & b1 is multiplicative & b1 is antimultiplicative )
set F = (Mor C) --> the Object of D;
the Object of D in Ob D ;
then reconsider F = (Mor C) --> the Object of D as Function of C,D by FUNCOP_1:45;
take F ; :: thesis: ( F is identity-preserving & F is multiplicative & F is antimultiplicative )
A2: for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
proof
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
reconsider x1 = f1, x2 = f2, x3 = f1 (*) f2 as object ;
A3: F . f1 = F . x1 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
A4: F . f2 = F . x2 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
A5: F . (f1 (*) f2) = F . x3 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
thus A6: F . f1 |> F . f2 by A3, A4, Th23; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)
thus F . (f1 (*) f2) = (F . f1) (*) (F . f2) by A4, A5, A3, A6, Th23; :: thesis: verum
end;
A7: for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) )
proof
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) )
assume f1 |> f2 ; :: thesis: ( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) )
reconsider x1 = f1, x2 = f2, x3 = f1 (*) f2 as object ;
A8: F . f1 = F . x1 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
A9: F . f2 = F . x2 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
A10: F . (f1 (*) f2) = F . x3 by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
thus A11: F . f2 |> F . f1 by A8, A9, Th23; :: thesis: F . (f1 (*) f2) = (F . f2) (*) (F . f1)
thus F . (f1 (*) f2) = (F . f2) (*) (F . f1) by A9, A10, A8, A11, Th23; :: thesis: verum
end;
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
reconsider x = f as object ;
F . f = F . x by A1, Def21
.= the Object of D by A1, FUNCOP_1:7 ;
hence F . f is identity by Th22; :: thesis: verum
end;
hence ( F is identity-preserving & F is multiplicative & F is antimultiplicative ) by A2, A7; :: thesis: verum
end;
suppose A12: C 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 )
A13: 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
the Function of C,D . f = the Object of D by A12, Def21;
hence the Function of C,D . f is identity by Th22; :: 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) ) ) ) by A12;
hence ( the Function of C,D is identity-preserving & the Function of C,D is multiplicative & the Function of C,D is antimultiplicative ) by A13; :: thesis: verum
end;
end;