let i be Element of NAT ; :: thesis: [!] . <*i*> = i !
defpred S2[ Nat] means [!] . <*$1*> = $1 ! ;
deffunc H1( Element of NAT , Element of NAT ) -> Element of NAT = $2;
deffunc H2( Element of NAT , Element of NAT ) -> Element of omega = $1 * $2;
deffunc H3( Element of NAT , Element of NAT ) -> Element of NAT = $1;
deffunc H4( Element of NAT ) -> Element of omega = $1 + 1;
set g = [*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>;
deffunc H5( Element of NAT , Element of NAT ) -> Element of omega = H4(H3($1,$2));
A1: for i, j being Element of NAT holds (2 proj 1) . <*i,j*> = H3(i,j)
proof
let i, j be Element of NAT ; :: thesis: (2 proj 1) . <*i,j*> = H3(i,j)
reconsider ij = <*i,j*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
thus (2 proj 1) . <*i,j*> = ij . 1 by Th37
.= i by FINSEQ_1:44 ; :: thesis: verum
end;
A2: for i being Element of NAT holds (1 succ 1) . <*i*> = H4(i)
proof
let i be Element of NAT ; :: thesis: (1 succ 1) . <*i*> = H4(i)
reconsider ij = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
thus (1 succ 1) . <*i*> = (ij /. 1) + 1 by Def7
.= i + 1 by FINSEQ_4:16 ; :: thesis: verum
end;
for i, j being Element of NAT holds ((1 succ 1) * <:<*(2 proj 1)*>:>) . <*i,j*> = H4(H3(i,j)) from COMPUT_1:sch 1(A2, A1);
 then A3: for i, j being Element of NAT holds ((1 succ 1) * <:<*(2 proj 1)*>:>) . <*i,j*> = H5(i,j) ;
A4: for i, j being Element of NAT holds (2 proj 2) . <*i,j*> = H1(i,j)
proof
let i, j be Element of NAT ; :: thesis: (2 proj 2) . <*i,j*> = H1(i,j)
reconsider ij = <*i,j*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
thus (2 proj 2) . <*i,j*> = ij . 2 by Th37
.= j by FINSEQ_1:44 ; :: thesis: verum
end;
A5: for i, j being Element of NAT holds [*] . <*i,j*> = H2(i,j) by Th85;
A6: for i, j being Element of NAT holds ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) . <*i,j*> = H2(H5(i,j),H1(i,j)) from COMPUT_1:sch 2(A5, A3, A4);
 A7: arity (0 const 1) = 0 by Th31;
A8: arity ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) = 2 by Def21;
A9: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider ie = i ! as Element of NAT ;
assume S2[i] ; :: thesis: S2[i + 1]
then [!] . <*(i1 + 1)*> = ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) . <*i1,ie*> by A8, A7, Th81
.= (i1 + 1) * ie by A6
.= (i + 1) ! by NEWTON:15 ;
hence S2[i + 1] ; :: thesis: verum
end;
0 -tuples_on NAT = {{}} by Th5;
then A10: {} in 0 -tuples_on NAT by TARSKI:def 1;
[!] . <*0*> = (0 const 1) . {} by A7, Th79
.= 0 ! by A10, FUNCOP_1:7, NEWTON:12 ;
then A11: S2[ 0 ] ;
for i being Nat holds S2[i] from NAT_1:sch 2(A11, A9);
 hence [!] . <*i*> = i ! ; :: thesis: verum