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 A4:
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;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

f /. n = f /. m ; :: thesis: f is constant

let n be Nat; :: according to SEQM_3:def 10 :: thesis: for b

( not n in dom f or not 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