hereby :: thesis: ( ex x being Element of X st
for n being Nat holds s . n = x implies s is constant )

assume s is constant ; :: thesis: ex x being Element of X st
for n being Nat holds s . n = x
then consider x being Element of X such that
A1: for n being Element of NAT st n in dom s holds
s . n = x by PARTFUN2:def 1;
take x = x; :: thesis: for n being Nat holds s . n = x
let n be Nat; :: thesis: s . n = x
( dom s = NAT & n in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;
hence s . n = x by A1; :: thesis: verum

end;

given x being Element of X such that A2: for n being Nat holds s . n = x ; :: thesis: s is constant
take x ; :: according to PARTFUN2:def 1 :: thesis: for b₁ being Element of NAT holds
( not b₁ in dom s or s . b₁ = x )
let n be Element of NAT ; :: thesis: ( not n in dom s or s . n = x )
assume n in dom s ; :: thesis: s . n = x
thus s . n = x by A2; :: thesis: verum