let F1, F2 be Function of the carrier of C,the carrier of D; :: thesis: ( ( for c being Element of the carrier of C
for d being Element of the carrier of D st F . (the Id of C . c) = the Id of D . d holds
F1 . c = d ) & ( for c being Element of the carrier of C
for d being Element of the carrier of D st F . (the Id of C . c) = the Id of D . d holds
F2 . c = d ) implies F1 = F2 )
assume that
A5: for c being Element of the carrier of C
for d being Element of the carrier of D st F . (the Id of C . c) = the Id of D . d holds
F1 . c = d and
A6: for c being Element of the carrier of C
for d being Element of the carrier of D st F . (the Id of C . c) = the Id of D . d holds
F2 . c = d ; :: thesis: F1 = F2
for c being Element of the carrier of C holds F1 . c = F2 . c

proof

let c be Element of the carrier of C; :: thesis: F1 . c = F2 . c
consider d1 being Element of the carrier of D such that
A7: F . (the Id of C . c) = the Id of D . d1 by A1;
consider d2 being Element of the carrier of D such that
A8: F . (the Id of C . c) = the Id of D . d2 by A1;
( id d1 = the Id of D . d1 & id d2 = the Id of D . d2 & dom (id d1) = d1 & dom (id d2) = d2 & c is Object of C ) by Def8;
then ( F1 . c = d1 & F2 . c = d2 & d1 = d2 ) by A5, A6, A7, A8;
hence F1 . c = F2 . c ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:113; :: thesis: verum