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