A1: dom s = NAT by PARTFUN1:def 2;
hereby :: thesis: ( ex x being set st
for n being Nat holds s . n = x implies s is constant )
assume A2: s is constant ; :: thesis: ex x being set st
for n being Nat holds s . n = x
take x = s . 0; :: thesis: for n being Nat holds s . n = x
let n be Nat; :: thesis: s . n = x
( 0 in dom s & n in dom s ) by A1, ORDINAL1:def 12;
hence s . n = x by A2; :: thesis: verum
end;
given x being set such that A3: for n being Nat holds s . n = x ; :: thesis: s is constant
let n1, n2 be object ; :: according to FUNCT_1:def 10 :: thesis: ( not n1 in dom s or not n2 in dom s or s . n1 = s . n2 )
assume A4: ( n1 in dom s & n2 in dom s ) ; :: thesis: s . n1 = s . n2
hence s . n1 = x by A3
.= s . n2 by A3, A4 ;
:: thesis: verum