let i, j be Element of 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 set ; :: 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:56;
then x = 2 proj 2 by TARSKI:def 1;
hence x in PrimRec by Def17; :: thesis: verum

end;

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

proof

let i, j be Element of NAT ; :: thesis: ( ([pred] * <:<*(2 proj 2)*>:>) . <*i,0 *> = 0 & ([pred] * <:<*(2 proj 2)*>:>) . <*i,(j + 1)*> = j )
reconsider i0 = <*i,0 *> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
reconsider ij = <*i,(j + 1)*> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
A2: dom (2 proj 2) = 2 -tuples_on NAT by Th40;
A3: dom <:F:> = dom (2 proj 2) by FUNCT_6:61;
hence ([pred] * <:<*(2 proj 2)*>:>) . <*i,0 *> = [pred] . (<:F:> . i0) by A2, FUNCT_1:23
.= [pred] . <*((2 proj 2) . i0)*> by A2, FUNCT_6:61
.= [pred] . <*(i0 . 2)*> by Th42
.= 0 by Th93, FINSEQ_1:61 ;
:: 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:23
.= [pred] . <*((2 proj 2) . ij)*> by A2, FUNCT_6:61
.= [pred] . <*(ij . 2)*> by Th42
.= [pred] . <*(j + 1)*> by FINSEQ_1:61
.= j by Th93 ; :: thesis: verum

end;

A4: now

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

A6: now

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:51;
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 13;
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;

[-] . <*i,(j + 1)*> = ((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)) . <*i,j,([-] . <*i,j*>)*> by Th85
.= i -' (j + 1) by A5, A6, Th87 ;
hence S₂[j + 1] ; :: thesis: verum

end;

reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:118;
[-] . <*i,0 *> = (1 proj 1) . <*i*> by Th83
.= ii . 1 by Th42
.= i by FINSEQ_1:57
.= (i + 0 ) -' 0 by NAT_D:34
.= i -' 0 ;
then A11: S₂[ 0 ] ;
for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A11, A4);
hence [-] . <*i,j*> = i -' j ; :: thesis: verum