let m, n be Nat; :: thesis: for l being Nat st 1 <= l & l <= n holds

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

set F = Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= n & (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . $1 <> m + $1 );

set rF = { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ;

A1: { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } c= Seg (m + n)

assume ex l being Nat st S_{1}[l]
; :: thesis: contradiction

then A5: ex l being Nat st S_{1}[l]
;

consider k being Nat such that

A6: S_{1}[k]
and

A7: for nn being Nat st S_{1}[nn] holds

k <= nn from NAT_1:sch 5(A5);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: m + k <= m + n by A6, XREAL_1:7;

reconsider Fk = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . k as Element of NAT by ORDINAL1:def 12;

A9: card rF = n

A13: rng (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) = rF by A1, FINSEQ_1:def 13;

m + 1 <= m + k by A6, XREAL_1:7;

then m + k in rF by A8;

then m + k in rng (Sgm rF) by A1, FINSEQ_1:def 13;

then consider x being object such that

A26: x in dom (Sgm rF) and

A27: m + k = (Sgm rF) . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A26;

A28: dom (Sgm rF) = Seg n by A1, A9, FINSEQ_3:40;

then A29: 1 <= x by A26, FINSEQ_1:1;

A30: x <= n by A28, A26, FINSEQ_1:1;

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

set F = Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ;

defpred S

set rF = { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ;

A1: { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } c= Seg (m + n)

proof

then reconsider rF = { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } as finite set ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } or x in Seg (m + n) )

assume x in { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ; :: thesis: x in Seg (m + n)

then consider x9 being Nat such that

A2: x9 = x and

A3: m + 1 <= x9 and

A4: x9 <= m + n ;

1 <= m + 1 by NAT_1:11;

then 1 <= x9 by A3, XXREAL_0:2;

hence x in Seg (m + n) by A2, A4; :: thesis: verum

end;assume x in { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ; :: thesis: x in Seg (m + n)

then consider x9 being Nat such that

A2: x9 = x and

A3: m + 1 <= x9 and

A4: x9 <= m + n ;

1 <= m + 1 by NAT_1:11;

then 1 <= x9 by A3, XXREAL_0:2;

hence x in Seg (m + n) by A2, A4; :: thesis: verum

assume ex l being Nat st S

then A5: ex l being Nat st S

consider k being Nat such that

A6: S

A7: for nn being Nat st S

k <= nn from NAT_1:sch 5(A5);

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: m + k <= m + n by A6, XREAL_1:7;

reconsider Fk = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . k as Element of NAT by ORDINAL1:def 12;

A9: card rF = n

proof
end;

then A12:
len (Sgm rF) = n
by A1, FINSEQ_3:39;per cases
( n = 0 or 0 < n )
;

end;

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

rF = {}

end;proof

hence
card rF = n
by A10; :: thesis: verum
assume
rF <> {}
; :: thesis: contradiction

then consider x being object such that

A11: x in rF by XBOOLE_0:def 1;

ex x9 being Nat st

( x9 = x & m + 1 <= x9 & x9 <= m + n ) by A11;

then m + 1 <= m + 0 by A10, XXREAL_0:2;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then consider x being object such that

A11: x in rF by XBOOLE_0:def 1;

ex x9 being Nat st

( x9 = x & m + 1 <= x9 & x9 <= m + n ) by A11;

then m + 1 <= m + 0 by A10, XXREAL_0:2;

hence contradiction by XREAL_1:6; :: thesis: verum

A13: rng (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) = rF by A1, FINSEQ_1:def 13;

now :: thesis: for k being Nat holds S_{2}[k]

then A25:
m + k <= Fk
by A6;defpred S_{2}[ Nat] means for Fk being Element of NAT st 1 <= $1 & $1 <= n & Fk = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . $1 holds

m + $1 <= Fk;

A14: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[ 0 ]
;

thus for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A24, A14); :: thesis: verum

end;m + $1 <= Fk;

A14: for k being Nat st S

S

proof

A24:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A15: S_{2}[k]
; :: thesis: S_{2}[k + 1]

A16: k < k + 1 by NAT_1:13;

let Fk1 be Element of NAT ; :: thesis: ( 1 <= k + 1 & k + 1 <= n & Fk1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) implies m + (k + 1) <= Fk1 )

assume that

A17: 1 <= k + 1 and

A18: k + 1 <= n and

A19: Fk1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) ; :: thesis: m + (k + 1) <= Fk1

end;assume A15: S

A16: k < k + 1 by NAT_1:13;

let Fk1 be Element of NAT ; :: thesis: ( 1 <= k + 1 & k + 1 <= n & Fk1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) implies m + (k + 1) <= Fk1 )

assume that

A17: 1 <= k + 1 and

A18: k + 1 <= n and

A19: Fk1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . (k + 1) ; :: thesis: m + (k + 1) <= Fk1

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

end;

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

reconsider Fk = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . k as Element of NAT by ORDINAL1:def 12;

A21: 1 <= k by A20, NAT_1:13;

k <= n by A18, NAT_1:13;

then A22: m + k <= Fk by A15, A21;

Fk < Fk1 by A1, A12, A18, A19, A16, A21, FINSEQ_1:def 13;

then m + k < Fk1 by A22, XXREAL_0:2;

then (m + k) + 1 <= Fk1 by NAT_1:13;

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

end;A21: 1 <= k by A20, NAT_1:13;

k <= n by A18, NAT_1:13;

then A22: m + k <= Fk by A15, A21;

Fk < Fk1 by A1, A12, A18, A19, A16, A21, FINSEQ_1:def 13;

then m + k < Fk1 by A22, XXREAL_0:2;

then (m + k) + 1 <= Fk1 by NAT_1:13;

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

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

then
1 in dom (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } )
by A12, A18, FINSEQ_3:25;

then (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . 1 in rng (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) by FUNCT_1:def 3;

then ex F1 being Nat st

( F1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . 1 & m + 1 <= F1 & F1 <= m + n ) by A13;

hence m + (k + 1) <= Fk1 by A19, A23; :: thesis: verum

end;then (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . 1 in rng (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) by FUNCT_1:def 3;

then ex F1 being Nat st

( F1 = (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . 1 & m + 1 <= F1 & F1 <= m + n ) by A13;

hence m + (k + 1) <= Fk1 by A19, A23; :: thesis: verum

thus for k being Nat holds S

m + 1 <= m + k by A6, XREAL_1:7;

then m + k in rF by A8;

then m + k in rng (Sgm rF) by A1, FINSEQ_1:def 13;

then consider x being object such that

A26: x in dom (Sgm rF) and

A27: m + k = (Sgm rF) . x by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A26;

A28: dom (Sgm rF) = Seg n by A1, A9, FINSEQ_3:40;

then A29: 1 <= x by A26, FINSEQ_1:1;

A30: x <= n by A28, A26, FINSEQ_1:1;