set f = ArProg (a,r);
let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in proj1 (ArProg (a,r)) or (ArProg (a,r)) . x is natural )
assume x in dom (ArProg (a,r)) ; :: thesis: (ArProg (a,r)) . x is natural
then reconsider i = x as Nat ;
defpred S₁[ Nat] means (ArProg (a,r)) . a is natural ;
A1: S₁[ 0 ] by NUMBER06:def 4;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
(ArProg (a,r)) . (k + 1) = ((ArProg (a,r)) . k) + r by NUMBER06:def 4;
hence ( S₁[k] implies S₁[k + 1] ) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
then S₁[i] ;
hence (ArProg (a,r)) . x is natural ; :: thesis: verum