let n1, n2 be Function of G,(G ./. N); :: thesis: ( ( for a being Element of G holds n1 . a = a * N ) & ( for a being Element of G holds n2 . a = a * N ) implies n1 = n2 )
assume that
A7: for a being Element of G holds n1 . a = a * N and
A8: for a being Element of G holds n2 . a = a * N ; :: thesis: n1 = n2

now :: thesis: for a being Element of G holds n1 . a = n2 . a

let a be Element of G; :: thesis: n1 . a = n2 . a
n1 . a = a * N by A7;
hence n1 . a = n2 . a by A8; :: thesis: verum

end;

hence n1 = n2 ; :: thesis: verum