set f = constF m;
for x1, x2 being object st x1 in NAT & x2 in NAT & (constF m) . x1 = (constF m) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & (constF m) . x1 = (constF m) . x2 implies x1 = x2 )
assume that
A1: ( x1 in NAT & x2 in NAT ) and
A2: (constF m) . x1 = (constF m) . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A1;
A3: (constF m) . x1 = m const x1 by Def16;
(constF m) . x2 = m const x2 by Def16;
hence x1 = x2 by A2, A3, Th45; :: thesis: verum

end;

hence constF m is one-to-one by FUNCT_2:19; :: thesis: verum