hereby :: thesis: ( ( for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m ) implies f is constant )

assume A1: f is constant ; :: thesis: for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m
let n, m be Nat; :: thesis: ( n in dom f & m in dom f implies f /. n = f /. m )
assume that
A2: n in dom f and
A3: m in dom f ; :: thesis: f /. n = f /. m
thus f /. n = f . n by A2, PARTFUN1:def 6
.= f . m by A1, A2, A3
.= f /. m by A3, PARTFUN1:def 6 ; :: thesis: verum

end;

assume A4: for n, m being Nat st n in dom f & m in dom f holds
f /. n = f /. m ; :: thesis: f is constant
let n be Nat; :: according to SEQM_3:def 10 :: thesis: for b₁ being set holds
( not n in dom f or not b₁ in dom f or f . n = f . b₁ )
let m be Nat; :: thesis: ( not n in dom f or not m in dom f or f . n = f . m )
assume that
A5: n in dom f and
A6: m in dom f ; :: thesis: f . n = f . m
thus f . n = f /. n by A5, PARTFUN1:def 6
.= f /. m by A4, A5, A6
.= f . m by A6, PARTFUN1:def 6 ; :: thesis: verum