deffunc H₁( Nat) -> set = p ^ <*($1 - 1)*>;
consider q being FinSequence such that
A1: ( len q = card (succ p) & ( for i being Nat st i in dom q holds
q . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A4: for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*>

proof

let i be Element of NAT ; :: thesis: ( i < len q implies q . (i + 1) = p ^ <*i*> )
assume i < len q ; :: thesis: q . (i + 1) = p ^ <*i*>
then q . (i + 1) = p ^ <*((i + 1) - 1)*> by A1, Lm3;
hence q . (i + 1) = p ^ <*i*> ; :: thesis: verum

end;

A5: q is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom q or not x2 in dom q or not q . x1 = q . x2 or x1 = x2 )
assume A6: ( x1 in dom q & x2 in dom q ) ; :: thesis: ( not q . x1 = q . x2 or x1 = x2 )
then reconsider i1 = x1, i2 = x2 as Element of NAT ;
( (p ^ <*(i1 - 1)*>) . ((len p) + 1) = i1 - 1 & (p ^ <*(i2 - 1)*>) . ((len p) + 1) = i2 - 1 & q . x1 = p ^ <*(i1 - 1)*> & q . x2 = p ^ <*(i2 - 1)*> ) by A1, A6, FINSEQ_1:59;
hence ( not q . x1 = q . x2 or x1 = x2 ) ; :: thesis: verum

end;

A7: rng q c= succ p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in succ p )
assume x in rng q ; :: thesis: x in succ p
then consider k being Element of NAT such that
A8: ( k < len q & x = q . (k + 1) ) by Lm4;
x = p ^ <*k*> by A4, A8;
hence x in succ p by A1, A8, Th7; :: thesis: verum

end;

then reconsider q = q as one-to-one FinSequence of succ p by A5, FINSEQ_1:def 4;
take q ; :: thesis: ( len q = card (succ p) & rng q = succ p & ( for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> ) )
thus ( len q = card (succ p) & rng q c= succ p ) by A1, A7; :: according to XBOOLE_0:def 10 :: thesis: ( succ p c= rng q & ( for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> ) )
thus succ p c= rng q :: thesis: for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*>

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ p or x in rng q )
assume A9: x in succ p ; :: thesis: x in rng q
then consider n being Element of NAT such that
A10: ( x = p ^ <*n*> & p ^ <*n*> in t ) ;
n < card (succ p) by A9, A10, Th7;
then ( q . (n + 1) = x & q . (n + 1) in rng q ) by A1, A4, A10, Lm3;
hence x in rng q ; :: thesis: verum

end;

thus for i being Element of NAT st i < len q holds
q . (i + 1) = p ^ <*i*> by A4; :: thesis: verum