let h1, h2 be Function of V,(Maps V); :: thesis: ( ( for A being Element of V holds h1 . A = id$ A ) & ( for A being Element of V holds h2 . A = id$ A ) implies h1 = h2 )
assume that
A21: for A being Element of V holds h1 . A = id$ A and
A22: for A being Element of V holds h2 . A = id$ A ; :: thesis: h1 = h2

now

let A be Element of V; :: thesis: h1 . A = h2 . A
thus h1 . A = id$ A by A21
.= h2 . A by A22 ; :: thesis: verum

end;

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