let X be set ; :: thesis: ( X is included_in_Seg implies for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds
m <= n )
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 is included_in_Seg ; :: thesis: for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds
m <= n

now :: thesis: for x being non zero Nat st S₁[x] holds
S₁[x + 1]

let x be non zero Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A2: S₁[x] ; :: thesis: S₁[x + 1]

now :: thesis: S₁[x + 1]

per cases ( ( x in dom (Sgm X) & ex n being Element of NAT st
( n = (Sgm X) . x & x <= n ) ) or not x in dom (Sgm X) ) by A2;

suppose A3: ( x in dom (Sgm X) & ex n being Element of NAT st
( n = (Sgm X) . x & x <= n ) ) ; :: thesis: S₁[x + 1]

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;

now :: thesis: ( x + 1 in dom (Sgm X) implies ex n1 being Element of NAT st
( n1 = (Sgm X) . (x + 1) & x + 1 <= n1 ) )

set n1 = (Sgm X) . (x + 1);
assume A8: x + 1 in dom (Sgm X) ; :: thesis: ex n1 being Element of NAT st
( n1 = (Sgm X) . (x + 1) & x + 1 <= n1 )
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: ( n1 = (Sgm X) . (x + 1) & x + 1 <= n1 )
thus n1 = (Sgm X) . (x + 1) ; :: thesis: x + 1 <= n1
x + 1 <= len (Sgm X) by A8, Th25;
then n < n1 by A1, A7, A4, A5, FINSEQ_1:def 14;
then x < n1 by A6, XXREAL_0:2;
hence x + 1 <= n1 by NAT_1:13; :: thesis: verum

end;

hence S₁[x + 1] ; :: thesis: verum

end;

suppose not x in dom (Sgm X) ; :: thesis: S₁[x + 1]

then ( x < 0 + 1 or x > len (Sgm X) ) by Th25;
then x + 1 > (len (Sgm X)) + 0 by NAT_1:13;
hence S₁[x + 1] by Th25; :: thesis: verum

end;

end;

end;

hence S₁[x + 1] ; :: thesis: verum

end;

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

now :: thesis: ( 1 in dom (Sgm X) & ex n being Element of NAT st
( n = (Sgm X) . 1 & 1 <= n ) )

set n = (Sgm X) . 1;
A12: m <= len (Sgm X) by A10, Th25;
1 <= m by A10, Th25;
then 1 <= len (Sgm X) by A12, XXREAL_0:2;
hence 1 in dom (Sgm X) by Th25; :: thesis: ex n being Element of NAT st
( n = (Sgm X) . 1 & 1 <= n )
then A13: (Sgm X) . 1 in rng (Sgm X) by FUNCT_1:3;
then reconsider n = (Sgm X) . 1 as Element of NAT ;
take n = n; :: thesis: ( n = (Sgm X) . 1 & 1 <= n )
thus n = (Sgm X) . 1 ; :: thesis: 1 <= n
A15: ex k being Nat st X c= Seg k by A1, FINSEQ_1:def 13;
rng (Sgm X) = X by A1, FINSEQ_1:def 14;
hence 1 <= n by A13, A15, FINSEQ_1:1; :: thesis: verum

end;

then A14: S₁[1] ;
for x being non zero Nat holds S₁[x] from NAT_1:sch 10(A14, A9);
then S₁[m9] ;
hence m <= n by A10, A11; :: thesis: verum