assume A1: z <> 0c ; :: thesis:
defpred S₁[ set ] means (z ExpSeq) . z <> 0c ;
A2: S₁[ 0 ] by Th3;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

assume (z ExpSeq) . (n + 1) = 0c ; :: thesis:
then A5: (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) = 0c by Th3;
0c = 0c / z
.= (((z ExpSeq) . n) * z) / z by A5, XCMPLX_1:50
.= ((z ExpSeq) . n) * (z / z)
.= ((z ExpSeq) . n) * 1 by A1, XCMPLX_1:60
.= (z ExpSeq) . n ;
hence contradiction by A4; :: thesis:

end;

deffunc H₁( Nat) -> Element of REAL = (|.(z ExpSeq).| . (z + 1)) / (|.(z ExpSeq).| . z);
thus A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3); :: thesis:
ex rseq being Real_Sequence st
for n being Nat holds rseq . n = H₁(n) from SEQ_1:sch 1();
then consider rseq being Real_Sequence such that
A7: for n being Nat holds rseq . n = (|.(z ExpSeq).| . (n + 1)) / (|.(z ExpSeq).| . n) ;

end;

end;