let m, n be Element of NAT ; :: thesis: ( m <= n implies PrimRec-Approximation . m c= PrimRec-Approximation . n )
set prd = PrimRec-Approximation ;
defpred S2[ Element of NAT ] means ( m <= $1 implies PrimRec-Approximation . m c= PrimRec-Approximation . $1 );
A1: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume that
A2: S2[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 Def23;
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, XBOOLE_1:1;
per cases ( m < n + 1 or m = n + 1 ) by A3, XXREAL_0:1;
end;
end;
A6: S2[ 0 ] ;
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A6, A1);
 hence ( m <= n implies PrimRec-Approximation . m c= PrimRec-Approximation . n ) ; :: thesis: verum