let i, j be Nat; :: thesis: [-] . <*i,j*> = i -' j
set F = <*(2 proj 2)*>;
set g = [pred] * <:<*(2 proj 2)*>:>;
rng <*(2 proj 2)*> c= PrimRec

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*(2 proj 2)*> or x in PrimRec )
assume x in rng <*(2 proj 2)*> ; :: thesis: x in PrimRec
then x in {(2 proj 2)} by FINSEQ_1:39;
then x = 2 proj 2 by TARSKI:def 1;
hence x in PrimRec by Def14; :: thesis: verum

end;

then reconsider F = <*(2 proj 2)*> as with_the_same_arity FinSequence of PrimRec by FINSEQ_1:def 4;
defpred S₂[ Nat] means [-] . <*i,$1*> = i -' $1;
A1: for i, j being Nat holds
( ([pred] * <:<*(2 proj 2)*>:>) . <*i,0*> = 0 & ([pred] * <:<*(2 proj 2)*>:>) . <*i,(j + 1)*> = j )

proof

let i, j be Nat; :: thesis: ( ([pred] * <:<*(2 proj 2)*>:>) . <*i,0*> = 0 & ([pred] * <:<*(2 proj 2)*>:>) . <*i,(j + 1)*> = j )
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
reconsider i0 = <*i1,0*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
reconsider ij = <*i1,(j1 + 1)*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
A2: dom (2 proj 2) = 2 -tuples_on NAT by Th35;
A3: dom <:F:> = dom (2 proj 2) by FINSEQ_3:141;
hence ([pred] * <:<*(2 proj 2)*>:>) . <*i,0*> = [pred] . (<:F:> . i0) by A2, FUNCT_1:13
.= [pred] . <*((2 proj 2) . i0)*> by A2, FINSEQ_3:141
.= [pred] . <*(i0 . 2)*> by Th37
.= 0 by Th88 ;
:: thesis: ([pred] * <:<*(2 proj 2)*>:>) . <*i,(j + 1)*> = j
thus ([pred] * <:<*(2 proj 2)*>:>) . <*i,(j + 1)*> = [pred] . (<:F:> . ij) by A3, A2, FUNCT_1:13
.= [pred] . <*((2 proj 2) . ij)*> by A2, FINSEQ_3:141
.= [pred] . <*(ij . 2)*> by Th37
.= j by Th88 ; :: thesis: verum

end;

A4: now :: thesis: for j being Nat st S₂[j] holds
S₂[j + 1]

let j be Nat; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A5: S₂[j] ; :: thesis: S₂[j + 1]

A6: now :: thesis: ([pred] * <:<*(2 proj 2)*>:>) . <*i,(i -' j)*> = i -' (j + 1)

per cases ( i -' j = 0 or ex k being Nat st i -' j = k + 1 ) by NAT_1:6;

suppose A7: i -' j = 0 ; :: thesis: ([pred] * <:<*(2 proj 2)*>:>) . <*i,(i -' j)*> = i -' (j + 1)

then i <= j by NAT_D:36;
then i < j + 1 by NAT_1:13;
then A8: i - (j + 1) < 0 by XREAL_1:49;
thus ([pred] * <:<*(2 proj 2)*>:>) . <*i,(i -' j)*> = 0 by A1, A7
.= i -' (j + 1) by A8, XREAL_0:def 2 ; :: thesis: verum

end;

suppose ex k being Nat st i -' j = k + 1 ; :: thesis: ([pred] * <:<*(2 proj 2)*>:>) . <*i,(i -' j)*> = i -' (j + 1)

then consider k being Nat such that
A9: i -' j = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
i - j = k + 1 by A9, XREAL_0:def 2;
then A10: i - (j + 1) = k ;
thus ([pred] * <:<*(2 proj 2)*>:>) . <*i,(i -' j)*> = k by A1, A9
.= i -' (j + 1) by A10, XREAL_0:def 2 ; :: thesis: verum

end;

end;

end;

reconsider jj = j as Element of NAT by ORDINAL1:def 12;
[-] . <*i,(jj + 1)*> = ((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)) . <*i,jj,([-] . <*i,jj*>)*> by Th80
.= i -' (jj + 1) by A5, A6, Th82 ;
hence S₂[j + 1] ; :: thesis: verum

end;

reconsider i = i as Element of NAT by ORDINAL1:def 12;
reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:98;
[-] . <*i,0*> = (1 proj 1) . <*i*> by Th78
.= ii . 1 by Th37
.= (i + 0) -' 0 by NAT_D:34
.= i -' 0 ;
then A11: S₂[ 0 ] ;
for j being Nat holds S₂[j] from NAT_1:sch 2(A11, A4);
hence [-] . <*i,j*> = i -' j ; :: thesis: verum