let n, m be Element of NAT ; :: thesis: for l being Element of NAT st 1 <= l & l <= n holds
(Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l
set F = Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= n & (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . $1 <> m + $1 );
assume ex l being Element of NAT st S₁[l] ; :: thesis: contradiction
then A1: ex l being Nat st S₁[l] ;
consider k being Nat such that
A2: S₁[k] and
A3: for nn being Nat st S₁[nn] holds
k <= nn from NAT_1:sch 5(A1);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
set rF = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ;
A4: { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } c= Seg (m + n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } or x in Seg (m + n) )
assume x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ; :: thesis: x in Seg (m + n)
then consider x' being Element of NAT such that
A5: ( x' = x & m + 1 <= x' & x' <= m + n ) ;
1 <= m + 1 by NAT_1:11;
then 1 <= x' by A5, XXREAL_0:2;
hence x in Seg (m + n) by A5; :: thesis: verum

end;

then reconsider rF = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } as finite set ;
A6: card rF = n

proof

per cases ( n = 0 or 0 < n ) ;

suppose A7: n = 0 ; :: thesis: card rF = n

rF = {}

proof

assume rF <> {} ; :: thesis: contradiction
then consider x being set such that
A8: x in rF by XBOOLE_0:def 1;
consider x' being Element of NAT such that
A9: ( x' = x & m + 1 <= x' & x' <= m + n ) by A8;
m + 1 <= m + 0 by A7, A9, XXREAL_0:2;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

hence card rF = n by A7; :: thesis: verum

end;

suppose 0 < n ; :: thesis: card rF = n

then 0 + 1 <= n by NAT_1:13;
then 1 - 1 <= n - 1 by XREAL_1:11;
then n -' 1 = n - 1 by XREAL_0:def 2;
then reconsider n1 = n - 1 as Element of NAT ;
(m + 1) + n1 = m + n ;
then card rF = n1 + 1 by Th4;
hence card rF = n ; :: thesis: verum

end;

end;

end;

( m + 1 <= m + k & m + k <= m + n ) by A2, XREAL_1:9;
then A10: m + k in rF ;
A11: dom (Sgm rF) = Seg n by A4, A6, FINSEQ_3:45;
A12: len (Sgm rF) = n by A4, A6, FINSEQ_3:44;
A13: rng (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) = rF by A4, FINSEQ_1:def 13;
m + k in rng (Sgm rF) by A4, A10, FINSEQ_1:def 13;
then consider x being set such that
A14: ( x in dom (Sgm rF) & m + k = (Sgm rF) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A14;
reconsider Fk = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . k as Element of NAT ;

now

defpred S₂[ Nat] means for Fk being Element of NAT st 1 <= $1 & $1 <= n & Fk = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . $1 holds
m + $1 <= Fk;
A15: S₂[ 0 ] ;
A16: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A17: S₂[k] ; :: thesis: S₂[k + 1]
let Fk1 be Element of NAT ; :: thesis: ( 1 <= k + 1 & k + 1 <= n & Fk1 = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) implies m + (k + 1) <= Fk1 )
assume that
A18: 1 <= k + 1 and
A19: k + 1 <= n and
A20: Fk1 = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) ; :: thesis: m + (k + 1) <= Fk1
A21: k < k + 1 by NAT_1:13;

per cases ( 1 < k + 1 or 1 = k + 1 ) by A18, XXREAL_0:1;

suppose 1 < k + 1 ; :: thesis: m + (k + 1) <= Fk1

then A22: ( 1 <= k & k <= n ) by A19, NAT_1:13;
reconsider Fk = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . k as Element of NAT ;
A23: m + k <= Fk by A17, A22;
Fk < Fk1 by A4, A12, A19, A20, A21, A22, FINSEQ_1:def 13;
then m + k < Fk1 by A23, XXREAL_0:2;
then (m + k) + 1 <= Fk1 by NAT_1:13;
hence m + (k + 1) <= Fk1 ; :: thesis: verum

end;

suppose A24: 1 = k + 1 ; :: thesis: m + (k + 1) <= Fk1

then 1 in dom (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) by A12, A19, FINSEQ_3:27;
then (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . 1 in rng (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) by FUNCT_1:def 5;
then consider F1 being Element of NAT such that
A25: ( F1 = (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . 1 & m + 1 <= F1 & F1 <= m + n ) by A13;
thus m + (k + 1) <= Fk1 by A20, A24, A25; :: thesis: verum

end;

end;

end;

thus for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A15, A16); :: thesis: verum

end;

then A26: m + k <= Fk by A2;
A27: ( 1 <= x & x <= n ) by A11, A14, FINSEQ_1:3;

per cases ( k < x or k > x ) by A2, A14, XXREAL_0:1;

suppose k < x ; :: thesis: contradiction

hence contradiction by A2, A4, A12, A14, A26, A27, FINSEQ_1:def 13; :: thesis: verum

end;

suppose A28: k > x ; :: thesis: contradiction

(Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . x <> m + x by A2, A14, XCMPLX_1:2;
hence contradiction by A3, A27, A28; :: thesis: verum

end;

end;