let X be set ; :: thesis:
let k be Element of NAT ; :: thesis:
defpred S₁[ Nat] means ( ( $1 in dom (Sgm X) & ex n being Element of NAT st
( n = (Sgm X) . $1 & $1 <= n ) ) or not $1 in dom (Sgm X) );
assume A1: X c= Seg k ; :: thesis:

suppose A3: ( x in dom (Sgm X) & ex n being Element of NAT st
( n = (Sgm X) . x & x <= n ) ) ; :: thesis:

A4: x + 0 < x + 1 by XREAL_1:8;
consider n being Element of NAT such that
A5: n = (Sgm X) . x and
A6: x <= n by A3;
A7: 1 <= x by A3, Th25;

set n1 = (Sgm X) . (x + 1);
assume A8: x + 1 in dom (Sgm X) ; :: thesis:
then (Sgm X) . (x + 1) in rng (Sgm X) by FUNCT_1:3;
then reconsider n1 = (Sgm X) . (x + 1) as Element of NAT ;
take n1 = n1; :: thesis:
thus n1 = (Sgm X) . (x + 1) ; :: thesis:
x + 1 <= len (Sgm X) by A8, Th25;
then n < n1 by A1, A7, A4, A5, FINSEQ_1:def 13;
then x < n1 by A6, XXREAL_0:2;
hence x + 1 <= n1 by NAT_1:13; :: thesis:

end;

end;

end;

end;

then A9: for x being non zero Nat st S₁[x] holds
S₁[x + 1] ;
let m, n be Element of NAT ; :: thesis:
assume that
A10: m in dom (Sgm X) and
A11: n = (Sgm X) . m ; :: thesis:
reconsider m9 = m as non zero Element of NAT by A10, Th25;

end;