take f = ArProg (1,1); :: thesis: ( f is non-empty & f is natural-valued & f is increasing )
A3: f . 0 = 1 by NUMBER06:def 4;
for i being object st i in dom f holds
not f . i is empty

proof

let i be object ; :: thesis: ( i in dom f implies not f . i is empty )
assume i in dom f ; :: thesis: not f . i is empty
then i in NAT by FUNCT_2:def 1;
then reconsider j = i as Nat ;

per cases ( 0 = j or 0 < j ) ;

suppose 0 = j ; :: thesis: not f . i is empty

hence not f . i is empty by NUMBER06:def 4; :: thesis: verum

end;

suppose 0 < j ; :: thesis: not f . i is empty

hence not f . i is empty by A3, SEQM_3:9; :: thesis: verum

end;

end;

end;

hence ( f is non-empty & f is natural-valued & f is increasing ) by FUNCT_1:def 9; :: thesis: verum