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 ;
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 b1 being Element of omega holds
( not b1 in dom s or s . b1 = x )
thus for b1 being Element of omega holds
( not b1 in dom s or s . b1 = x ) by A2; :: thesis: verum