let f, g be Function of Q,(Q _/_ N); :: thesis: ( ( for x being Element of Q holds f . x = x * N ) & ( for x being Element of Q holds g . x = x * N ) implies f = g )
assume that
A5: for x being Element of Q holds f . x = x * N and
A6: for x being Element of Q holds g . x = x * N ; :: thesis: f = g
let x be Element of Q; :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
thus f . x = x * N by A5
.= g . x by A6 ; :: thesis: verum