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