let A, B be Element of NAT ; :: thesis: for X being non empty set
for F being Function of NAT ,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 Function of NAT ,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 Function of NAT ,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₁[ Element of 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;

now

let x be set ; :: 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
A3: ( F . w = x & A <= w & w <= A + 0 ) ;
w = A by A3, XXREAL_0:1;
hence x in {(F . A)} by A3, 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 A4: S₁[ 0 ] by CARD_1:50;
A5: 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 A6: S₁[k] ; :: thesis: S₁[k + 1]
set Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } ;
set Fwk1 = { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } ;
card { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } is finite by A6;
then reconsider Fwk = { (F . w) where w is Element of NAT : ( A <= w & w <= A + k ) } as finite set ;

now

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

end;

then A8: card (Fwk \/ {(F . ((A + k) + 1))}) = (k + 1) + 1 by A6, CARD_2:54;

now

let x be set ; :: 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
A9: ( x = F . w & A <= w & w <= (A + k) + 1 ) ;
A10: ( w = (A + k) + 1 or w < (A + k) + 1 ) by A9, XXREAL_0:1;

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

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

then x in {(F . ((A + k) + 1))} by A9, 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 A9;
hence x in Fwk \/ {(F . ((A + k) + 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume A11: 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 A11, 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
A12: ( x = F . w & A <= w & w <= A + k ) ;
w <= (A + k) + 1 by A12, NAT_1:13;
hence x in { (F . w) where w is Element of NAT : ( A <= w & w <= (A + k) + 1 ) } by A12; :: thesis: verum

end;

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

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

end;

end;

end;

hence S₁[k + 1] by A8, TARSKI:2; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
hence card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1 ; :: thesis: verum