let F1, F2 be Function of V,(Morphs V); :: thesis: ( ( for G being Element of V holds F1 . G = ID G ) & ( for G being Element of V holds F2 . G = ID G ) implies F1 = F2 )
assume that
A8: for G being Element of V holds F1 . G = ID G and
A9: for G being Element of V holds F2 . G = ID G ; :: thesis: F1 = F2

now

let G be Element of V; :: thesis: F1 . G = F2 . G
F1 . G = ID G by A8;
hence F1 . G = F2 . G by A9; :: thesis: verum

end;

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