let F, G be Function of the carrier of C, the carrier' of C; ( ( for o being Object of C holds F . o = id o ) & ( for o being Object of C holds G . o = id o ) implies F = G )
assume that
A2:
for o being Object of C holds F . o = id o
and
A3:
for o being Object of C holds G . o = id o
; F = G
let o be Object of C; FUNCT_2:def 8 F . o = G . o
thus F . o =
id o
by A2
.=
G . o
by A3
; verum