thus ( f is constant implies for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ) by FUNCT_1:def 10; :: thesis: ( ( for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ) implies f is constant )
assume A1: for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ; :: thesis: f is constant
let n, m be set ; :: according to FUNCT_1:def 10 :: thesis: ( not n in proj1 f or not m in proj1 f or f . n = f . m )
assume ( n in dom f & m in dom f ) ; :: thesis: f . n = f . m
hence f . n = f . m by A1; :: thesis: verum