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 . (id c) = id d holds
F1 . c = d ) & ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
F2 . c = d ) implies F1 = F2 )
assume that
A4: for c being Element of C
for d being Element of D st F . (id c) = id d holds
F1 . c = d and
A5: for c being Element of C
for d being Element of D st F . (id c) = id 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
A6: F . (id c) = id d1 by A1;
F1 . c = d1 by A4, A6;
hence F1 . c = F2 . c by A5, A6; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; :: thesis: verum