let i be Element of NAT ; :: thesis: [!] . <*i*> = i !
defpred S2[ Element of 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 NAT = $1 * $2;
deffunc H3( Element of NAT , Element of NAT ) -> Element of NAT = $1;
deffunc H4( Element of NAT ) -> Element of NAT = $1 + 1;
set g = [*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>;
deffunc H5( Element of NAT , Element of NAT ) -> Element of NAT = 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 Th42
.= 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 Def10
.= 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 Th42
.= j by FINSEQ_1:44 ; :: thesis: verum
end;
A5: for i, j being Element of NAT holds [*] . <*i,j*> = H2(i,j) by Th90;
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 Th35;
A8: arity ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) = 2 by Def24;
A9: now
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
reconsider ie = i ! as Element of NAT ;
assume S2[i] ; :: thesis: S2[i + 1]
then [!] . <*(i + 1)*> = ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) . <*i,ie*> by A8, A7, Th86
.= (i + 1) * ie by A6
.= (i + 1) ! by NEWTON:15 ;
hence S2[i + 1] ; :: thesis: verum
end;
0 -tuples_on NAT = {{}} by Th8;
then A10: {} in 0 -tuples_on NAT by TARSKI:def 1;
[!] . <*0*> = (0 const 1) . {} by A7, Th84
.= 0 ! by A10, FUNCOP_1:7, NEWTON:12 ;
then A11: S2[ 0 ] ;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A11, A9);
 hence [!] . <*i*> = i ! ; :: thesis: verum