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 S1[ 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)
proof
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;
then reconsider rF = { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } as finite set ;
a1: rF is included_in_Seg by A1;
assume ex l being Nat st S1[l] ; :: thesis: contradiction
then A5: ex l being Nat st S1[l] ;
consider k being Nat such that
A6: S1[k] and
A7: for nn being Nat st S1[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
proof
per cases ( n = 0 or 0 < n ) ;
suppose A10: n = 0 ; :: thesis: card rF = n
rF = {}
proof
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;
hence card rF = n by A10; :: 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:9;
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;
then A12: len (Sgm rF) = n by a1, FINSEQ_3:39;
A13: rng (Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) = rF by a1, FINSEQ_1:def 14;
now :: thesis: for k being Nat holds S2[k]
defpred S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A15: S2[k] ; :: thesis: S2[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
per cases ( 1 < k + 1 or 1 = k + 1 ) by A17, XXREAL_0:1;
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 14;
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;
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;
end;
end;
A24: S2[ 0 ] ;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A24, A14); :: thesis: verum
end;
then A25: m + k <= Fk by A6;
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 14;
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;
per cases ( k < x or k > x ) by A6, A27, XXREAL_0:1;
suppose k < x ; :: thesis: contradiction
hence contradiction by a1, A6, A12, A27, A25, A30, FINSEQ_1:def 14; :: thesis: verum
end;
suppose A31: k > x ; :: thesis: contradiction
(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . x <> m + x by A6, A27, XCMPLX_1:2;
hence contradiction by A7, A29, A30, A31; :: thesis: verum
end;
end;