let i, n be Nat; :: thesis: for P being non empty primitive-recursively_closed Subset of (HFuncs NAT) st 1 <= i & i <= n holds
n succ i in P
let P be non empty primitive-recursively_closed Subset of (HFuncs NAT); :: thesis: ( 1 <= i & i <= n implies n succ i in P )
A1: 1 succ 1 in P by Def14;
A2: arity (1 succ 1) = len <*(n proj i)*> by FINSEQ_1:39;
reconsider nproji = n proj i as Element of HFuncs NAT by Th27;
assume that
A3: 1 <= i and
A4: i <= n ; :: thesis: n succ i in P
A5: <*nproji*> is with_the_same_arity FinSequence of HFuncs NAT ;

now :: thesis: ( dom (n succ i) = n -tuples_on NAT & dom ((1 succ 1) * <:<*(n proj i)*>:>) = n -tuples_on NAT & ( for x being object st x in n -tuples_on NAT holds
(n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x ) )

rng (n proj i) = NAT by A3, A4, Th35;
then A6: rng <:<*(n proj i)*>:> = 1 -tuples_on NAT by Th8;
thus dom (n succ i) = n -tuples_on NAT by Def7; :: thesis: ( dom ((1 succ 1) * <:<*(n proj i)*>:>) = n -tuples_on NAT & ( for x being object st x in n -tuples_on NAT holds
(n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x ) )
A7: dom (n proj i) = n -tuples_on NAT by Th35;
then A8: dom <:<*(n proj i)*>:> = n -tuples_on NAT by FINSEQ_3:141;
dom (1 succ 1) = 1 -tuples_on NAT by Def7;
hence dom ((1 succ 1) * <:<*(n proj i)*>:>) = n -tuples_on NAT by A8, A6, RELAT_1:27; :: thesis: for x being object st x in n -tuples_on NAT holds
(n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x
let x be object ; :: thesis: ( x in n -tuples_on NAT implies (n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x )
assume x in n -tuples_on NAT ; :: thesis: (n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x
then reconsider x9 = x as Element of n -tuples_on NAT ;
set xi = x9 . i;
A10: (n succ i) . x = (x9 . i) + 1 by Def7;
reconsider ii = <*(x9 . i)*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
((1 succ 1) * <:<*(n proj i)*>:>) . x9 = (1 succ 1) . (<:<*(n proj i)*>:> . x9) by A8, FUNCT_1:13
.= (1 succ 1) . <*((n proj i) . x9)*> by A7, FINSEQ_3:141
.= (1 succ 1) . <*(x9 . i)*> by Th37
.= (ii . 1) + 1 by Def7
.= (x9 . i) + 1 ;
hence (n succ i) . x = ((1 succ 1) * <:<*(n proj i)*>:>) . x by A10; :: thesis: verum

end;

then A11: n succ i = (1 succ 1) * <:<*(n proj i)*>:> ;
A12: rng <*(n proj i)*> c= P

proof

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

end;

P is composition_closed by Def14;
hence n succ i in P by A11, A1, A2, A12, A5; :: thesis: verum