let f be Function; :: thesis: ( f is Integer_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds
f . x is integer ) ) )
thus ( f is Integer_Sequence implies ( dom f = NAT & ( for x being object st x in NAT holds
f . x is integer ) ) ) by SEQ_1:1; :: thesis: ( dom f = NAT & ( for x being object st x in NAT holds
f . x is integer ) implies f is Integer_Sequence )
assume that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x is integer ; :: thesis: f is Integer_Sequence
now :: thesis: for y being object st y in rng f holds
y in INT
let y be object ; :: thesis: ( y in rng f implies y in INT )
assume y in rng f ; :: thesis: y in INT
then consider x being object such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 3;
f . x is integer by A1, A2, A3;
hence y in INT by A4; :: thesis: verum
end;
then A5: rng f c= INT ;
for x being object st x in NAT holds
f . x is real
proof
let x be object ; :: thesis: ( x in NAT implies f . x is real )
assume x in NAT ; :: thesis: f . x is real
then f . x is integer by A2;
hence f . x is real ; :: thesis: verum
end;
hence f is Integer_Sequence by A1, A5, RELAT_1:def 19, SEQ_1:1; :: thesis: verum