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();
A2: q is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 q or not x2 in proj1 q or not q . x1 = q . x2 or x1 = x2 )
assume A3: ( x1 in dom q & x2 in dom q ) ; :: thesis: ( not q . x1 = q . x2 or x1 = x2 )
then reconsider i1 = x1, i2 = x2 as Nat ;
A4: ( (p ^ <*(i1 - 1)*>) . ((len p) + 1) = i1 - 1 & (p ^ <*(i2 - 1)*>) . ((len p) + 1) = i2 - 1 ) by FINSEQ_1:42;
( q . x1 = p ^ <*(i1 - 1)*> & q . x2 = p ^ <*(i2 - 1)*> ) by A1, A3;
hence ( not q . x1 = q . x2 or x1 = x2 ) by A4; :: thesis: verum

end;

A5: for i being Nat st i < len q holds
q . (i + 1) = p ^ <*i*>

proof

let i be 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;

A6: rng q c= succ p

proof

let x be object ; :: 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 Nat such that
A7: k < len q and
A8: x = q . (k + 1) by Lm4;
x = p ^ <*k*> by A5, A7, A8;
hence x in succ p by A1, A7, Th7; :: thesis: verum

end;

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

proof

let x be object ; :: 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 Nat such that
A10: x = p ^ <*n*> and
p ^ <*n*> in t ;
A11: n < card (succ p) by A9, A10, Th7;
then q . (n + 1) = x by A1, A5, A10;
hence x in rng q by A1, A11, Lm3; :: thesis: verum

end;

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