let i be Element of NAT ; :: thesis: [!] . <*i*> = i !
set g = [*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>;
deffunc H₁( Element of NAT ) -> Element of NAT = $1 + 1;
deffunc H₂( Element of NAT , Element of NAT ) -> Element of NAT = $1;
deffunc H₃( Element of NAT , Element of NAT ) -> Element of NAT = $1 * $2;
deffunc H₄( Element of NAT , Element of NAT ) -> Element of NAT = H₁(H₂($1,$2));
deffunc H₅( Element of NAT , Element of NAT ) -> Element of NAT = $2;
A1: for i, j being Element of NAT holds [*] . <*i,j*> = H₃(i,j) by Th90;
A2: for i being Element of NAT holds (1 succ 1) . <*i*> = H₁(i)

proof

let i be Element of NAT ; :: thesis: (1 succ 1) . <*i*> = H₁(i)
reconsider ij = <*i*> as Element of 1 -tuples_on NAT ;
thus (1 succ 1) . <*i*> = (ij /. 1) + 1 by Def10
.= i + 1 by FINSEQ_4:25 ; :: thesis: verum

end;

A3: for i, j being Element of NAT holds (2 proj 1) . <*i,j*> = H₂(i,j)

proof

let i, j be Element of NAT ; :: thesis: (2 proj 1) . <*i,j*> = H₂(i,j)
reconsider ij = <*i,j*> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
thus (2 proj 1) . <*i,j*> = ij . 1 by Th42
.= i by FINSEQ_1:61 ; :: thesis: verum

end;

for i, j being Element of NAT holds ((1 succ 1) * <:<*(2 proj 1)*>:>) . <*i,j*> = H₁(H₂(i,j)) from COMPUT_1:sch 1(A2, A3);
then A4: for i, j being Element of NAT holds ((1 succ 1) * <:<*(2 proj 1)*>:>) . <*i,j*> = H₄(i,j) ;
A5: for i, j being Element of NAT holds (2 proj 2) . <*i,j*> = H₅(i,j)

proof

let i, j be Element of NAT ; :: thesis: (2 proj 2) . <*i,j*> = H₅(i,j)
reconsider ij = <*i,j*> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
thus (2 proj 2) . <*i,j*> = ij . 2 by Th42
.= j by FINSEQ_1:61 ; :: thesis: verum

end;

A6: for i, j being Element of NAT holds ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) . <*i,j*> = H₃(H₄(i,j),H₅(i,j)) from COMPUT_1:sch 2(A1, A4, A5);
A7: arity ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) = 2 by Def26;
A8: arity (0 const 1) = 0 by Th35;
0 -tuples_on NAT = {{} } by Th8;
then A9: {} in 0 -tuples_on NAT by TARSKI:def 1;
defpred S₂[ Element of NAT ] means [!] . <*$1*> = $1 ! ;
A10: S₂[ 0 ]

proof

thus [!] . <*0 *> = (0 const 1) . {} by A8, Th84
.= 0 ! by A9, FUNCOP_1:13, NEWTON:18 ; :: thesis: verum

end;

A11: now

let i be Element of NAT ; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A12: S₂[i] ; :: thesis: S₂[i + 1]
reconsider ie = i ! as Element of NAT ;
[!] . <*(i + 1)*> = ([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>) . <*i,ie*> by A7, A8, A12, Th86
.= (i + 1) * ie by A6
.= (i + 1) ! by NEWTON:21 ;
hence S₂[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A10, A11);
hence [!] . <*i*> = i ! ; :: thesis: verum