let f be Arithmetic_Progression; :: thesis: f = ArProg ((f . 0),(difference f))
set a = f . 0;
set r = (f . 1) - (f . 0);
defpred S₁[ Nat] means f . $1 = (ArProg ((f . 0),((f . 1) - (f . 0)))) . $1;
A2: S₁[ 0 ] by ArDefRec;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume a5: S₁[k] ; :: thesis: S₁[k + 1]
(f . (k + 1)) - (f . k) = (f . 1) - (f . 0) by LemmaDiffConst;
then f . (k + 1) = (f . k) + ((f . 1) - (f . 0)) ;
hence S₁[k + 1] by a5, ArDefRec; :: thesis: verum

end;

S1: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
for n being Element of NAT holds f . n = (ArProg ((f . 0),((f . 1) - (f . 0)))) . n by S1;
hence f = ArProg ((f . 0),(difference f)) by FUNCT_2:def 8; :: thesis: verum