let h1, h2 be Function of (CSp X),(MapsC X); :: thesis: ( ( for C being Element of CSp X holds h1 . C = id$ C ) & ( for C being Element of CSp X holds h2 . C = id$ C ) implies h1 = h2 )
assume that
A22: for C being Element of CSp X holds h1 . C = id$ C and
A23: for C being Element of CSp X holds h2 . C = id$ C ; :: thesis: h1 = h2

now

let C be Element of CSp X; :: thesis: h1 . C = h2 . C
thus h1 . C = id$ C by A22
.= h2 . C by A23 ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:63; :: thesis: verum