consider d being Element of D;
reconsider F = the carrier' of C --> (the Id of D . d) as Function of the carrier' of C,the carrier' of D ;
take F ; :: thesis: ( ( for c being Element of C ex d being Element of D st F . (the Id of C . c) = the Id of D . d ) & ( for f being Element of the carrier' of C holds
( F . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (F . f)) & F . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (the Comp of C . g,f) = the Comp of D . (F . g),(F . f) ) )
thus for c being Element of C ex d being Element of D st F . (the Id of C . c) = the Id of D . d by FUNCOP_1:13; :: thesis: ( ( for f being Element of the carrier' of C holds
( F . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (F . f)) & F . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (F . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (the Comp of C . g,f) = the Comp of D . (F . g),(F . f) ) )
A1: Hom d,d <> {} by Th55;
thus for f being Element of the carrier' of C holds
( F . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (F . f)) & F . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (F . f)) ) :: thesis: for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
F . (the Comp of C . g,f) = the Comp of D . (F . g),(F . f)

proof

let f be Element of the carrier' of C; :: thesis: ( F . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (F . f)) & F . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (F . f)) )
A2: F . f = the Id of D . d by FUNCOP_1:13;
thus F . (the Id of C . (the Source of C . f)) = the Id of D . d by FUNCOP_1:13
.= the Id of D . (the Source of D . (F . f)) by A2, Def8 ; :: thesis: F . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (F . f))
thus F . (the Id of C . (the Target of C . f)) = the Id of D . d by FUNCOP_1:13
.= the Id of D . (the Target of D . (F . f)) by A2, Def8 ; :: thesis: verum

end;

let f, g be Element of the carrier' of C; :: thesis: ( [g,f] in dom the Comp of C implies F . (the Comp of C . g,f) = the Comp of D . (F . g),(F . f) )
assume A3: [g,f] in dom the Comp of C ; :: thesis: F . (the Comp of C . g,f) = the Comp of D . (F . g),(F . f)
set f9 = F . f;
F . f = the Id of D . d by FUNCOP_1:13;
then A4: the Target of D . (F . f) = d by Def8;
F . g = the Id of D . d by FUNCOP_1:13;
then the Source of D . (F . g) = d by Def8;
then A5: [(F . g),(F . f)] in dom the Comp of D by A4, Def8;
thus F . (the Comp of C . g,f) = the Id of D . d by A3, FUNCOP_1:13, PARTFUN1:27
.= (id d) * (id d) by Th59
.= (id d) * (id d) by A1, Def13
.= (id d) * (F . f) by FUNCOP_1:13
.= (F . g) * (F . f) by FUNCOP_1:13
.= the Comp of D . (F . g),(F . f) by A5, Def4 ; :: thesis: verum