let m, n be Nat; :: thesis: ( m <= n implies PrimRec-Approximation . m c= PrimRec-Approximation . n )
set prd = PrimRec-Approximation ;
defpred S₂[ Nat] means ( m <= $1 implies PrimRec-Approximation . m c= PrimRec-Approximation . $1 );
A1: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume that
A2: S₂[n] and
A3: m <= n + 1 ; :: thesis: PrimRec-Approximation . m c= PrimRec-Approximation . (n + 1)
PrimRec-Approximation . (n + 1) = (PR-closure (PrimRec-Approximation . n)) \/ (composition-closure (PrimRec-Approximation . n)) by Def20;
then A4: PR-closure (PrimRec-Approximation . n) c= PrimRec-Approximation . (n + 1) by XBOOLE_1:7;
PrimRec-Approximation . n c= PR-closure (PrimRec-Approximation . n) by XBOOLE_1:7;
then A5: PrimRec-Approximation . n c= PrimRec-Approximation . (n + 1) by A4;

per cases ( m < n + 1 or m = n + 1 ) by A3, XXREAL_0:1;

suppose m < n + 1 ; :: thesis: PrimRec-Approximation . m c= PrimRec-Approximation . (n + 1)

hence PrimRec-Approximation . m c= PrimRec-Approximation . (n + 1) by A2, A5, NAT_1:13; :: thesis: verum

end;

suppose m = n + 1 ; :: thesis: PrimRec-Approximation . m c= PrimRec-Approximation . (n + 1)

hence PrimRec-Approximation . m c= PrimRec-Approximation . (n + 1) ; :: thesis: verum

end;

end;

end;

A6: S₂[ 0 ] ;
for n being Nat holds S₂[n] from NAT_1:sch 2(A6, A1);
hence ( m <= n implies PrimRec-Approximation . m c= PrimRec-Approximation . n ) ; :: thesis: verum