set d = the Element of D;
reconsider F = the carrier' of C --> (id the Element of D) as Function of the carrier' of C, the carrier' of D ;
take
F
; ( ( for c being Element of C ex d being Element of D st F . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
thus
for c being Element of C ex d being Element of D st F . (id c) = id d
by FUNCOP_1:7; ( ( for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f) ) )
A1:
Hom ( the Element of D, the Element of D) <> {}
;
thus
for f being Element of the carrier' of C holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (g (*) f) = (F . g) (*) (F . f)
let f, g be Element of the carrier' of C; ( [g,f] in dom the Comp of C implies F . (g (*) f) = (F . g) (*) (F . f) )
assume
[g,f] in dom the Comp of C
; F . (g (*) f) = (F . g) (*) (F . f)
thus F . (g (*) f) =
(id the Element of D) * (id the Element of D)
by FUNCOP_1:7
.=
(id the Element of D) (*) (id the Element of D)
by A1, Def11
.=
(id the Element of D) (*) (F . f)
by FUNCOP_1:7
.=
(F . g) (*) (F . f)
by FUNCOP_1:7
; verum