let A, B be Element of NAT ; :: thesis: for X being non empty set
for F being sequence of X st F is one-to-one holds
card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1
let X be non empty set ; :: thesis: for F being sequence of X st F is one-to-one holds
card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1
let F be sequence of X; :: thesis: ( F is one-to-one implies card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1 )
assume A1: F is one-to-one ; :: thesis: card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1
defpred S₁[ Nat] means card { (F . w) where w is Element of NAT : ( A <= w & w <= A + $1 ) } = $1 + 1;
A2: dom F = NAT by FUNCT_2:def 1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } ;
reconsider Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } as finite set by A4;
set Fwk1 = { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } ;

A5: now :: thesis: for x being object holds
( ( x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } implies x in Fwk \/ {(F . ((A + k) + 1))} ) & ( x in Fwk \/ {(F . ((A + k) + 1))} implies x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } ) )

let x be object ; :: thesis: ( ( x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } implies x in Fwk \/ {(F . ((A + k) + 1))} ) & ( x in Fwk \/ {(F . ((A + k) + 1))} implies b₁ in { (F . b₂) where w is Element of NAT : ( A <= b₂ & b₂ <= (A + k) + 1 ) } ) )

hereby :: thesis: ( x in Fwk \/ {(F . ((A + k) + 1))} implies b₁ in { (F . b₂) where w is Element of NAT : ( A <= b₂ & b₂ <= (A + k) + 1 ) } )

assume x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } ; :: thesis: x in Fwk \/ {(F . ((A + k) + 1))}
then consider w being Element of NAT such that
A6: x = F . w and
A7: A <= w and
A8: w <= (A + k) + 1 ;
A9: ( w = (A + k) + 1 or w < (A + k) + 1 ) by A8, XXREAL_0:1;

per cases ( w = (A + k) + 1 or w <= A + k ) by A9, NAT_1:13;

suppose w = (A + k) + 1 ; :: thesis: x in Fwk \/ {(F . ((A + k) + 1))}

then x in {(F . ((A + k) + 1))} by A6, TARSKI:def 1;
hence x in Fwk \/ {(F . ((A + k) + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose w <= A + k ; :: thesis: x in Fwk \/ {(F . ((A + k) + 1))}

then x in Fwk by A6, A7;
hence x in Fwk \/ {(F . ((A + k) + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A10: x in Fwk \/ {(F . ((A + k) + 1))} ; :: thesis: b₁ in { (F . b₂) where w is Element of NAT : ( A <= b₂ & b₂ <= (A + k) + 1 ) }

per cases ( x in Fwk or x in {(F . ((A + k) + 1))} ) by A10, XBOOLE_0:def 3;

suppose x in Fwk ; :: thesis: b₁ in { (F . b₂) where w is Element of NAT : ( A <= b₂ & b₂ <= (A + k) + 1 ) }

then consider w being Element of NAT such that
A11: x = F . w and
A12: A <= w and
A13: w <= A + k ;
w <= (A + k) + 1 by A13, NAT_1:13;
hence x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } by A11, A12; :: thesis: verum

end;

suppose A14: x in {(F . ((A + k) + 1))} ; :: thesis: b₁ in { (F . b₂) where w is Element of NAT : ( A <= b₂ & b₂ <= (A + k) + 1 ) }

A15: A <= A + (k + 1) by NAT_1:11;
x = F . ((A + k) + 1) by A14, TARSKI:def 1;
hence x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } by A15; :: thesis: verum

end;

end;

end;

now :: thesis: not F . ((A + k) + 1) in Fwk

assume F . ((A + k) + 1) in Fwk ; :: thesis: contradiction
then consider w being Element of NAT such that
A16: F . ((A + k) + 1) = F . w and
A <= w and
A17: w <= A + k ;
(A + k) + 1 = w by A1, A2, A16, FUNCT_1:def 4;
hence contradiction by A17, NAT_1:13; :: thesis: verum

end;

then card (Fwk \/ {(F . ((A + k) + 1))}) = (k + 1) + 1 by A4, CARD_2:41;
hence S₁[k + 1] by A5, TARSKI:2; :: thesis: verum

end;

now :: thesis: for x being object holds
( ( x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } implies x in {(F . A)} ) & ( x in {(F . A)} implies x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } ) )

let x be object ; :: thesis: ( ( x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } implies x in {(F . A)} ) & ( x in {(F . A)} implies x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } ) )

hereby :: thesis: ( x in {(F . A)} implies x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } )

assume x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } ; :: thesis: x in {(F . A)}
then consider w being Element of NAT such that
A18: F . w = x and
A19: A <= w and
A20: w <= A + 0 ;
w = A by A19, A20, XXREAL_0:1;
hence x in {(F . A)} by A18, TARSKI:def 1; :: thesis: verum

end;

assume x in {(F . A)} ; :: thesis: x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) }
then x = F . A by TARSKI:def 1;
hence x in { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } ; :: thesis: verum

end;

then { (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } = {(F . A)} by TARSKI:2;
then A21: S₁[ 0 ] by CARD_1:30;
for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A3);
hence card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1 ; :: thesis: verum