let F1, F2 be Function of the carrier of C, the carrier of D; :: thesis: ( ( for c being Element of C
for d being Element of D st F . ( the Id of C . c) = the Id of D . d holds
F1 . c = d ) & ( for c being Element of C
for d being Element 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 C
for d being Element 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 C
for d being Element 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 C holds F1 . c = F2 . c

proof

let c be Element of C; :: thesis: F1 . c = F2 . c
consider d1 being Element of D such that
A7: F . ( the Id of C . c) = the Id of D . d1 by A1;
F1 . c = d1 by A5, A7;
hence F1 . c = F2 . c by A6, A7; :: thesis: verum

end;

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