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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

then A21: S_{1}[ 0 ]
by CARD_1:30;

for k being Nat holds S_{1}[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

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

A2: dom F = NAT by FUNCT_2:def 1;

A3: for k being Nat st S

S

proof

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

assume A4: S_{1}[k]
; :: thesis: S_{1}[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 ) } ;

hence S_{1}[k + 1]
by A5, TARSKI:2; :: thesis: verum

end;assume A4: S

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 ) } ) )

( ( 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_{1} in { (F . b_{2}) where w is Element of NAT : ( A <= b_{2} & b_{2} <= (A + k) + 1 ) } ) )

_{1} in { (F . b_{2}) where w is Element of NAT : ( A <= b_{2} & b_{2} <= (A + k) + 1 ) }

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

assume A10:
x in Fwk \/ {(F . ((A + k) + 1))}
; :: thesis: bassume
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;

end;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
( x in Fwk or x in {(F . ((A + k) + 1))} )
by A10, XBOOLE_0:def 3;

end;

suppose
x in Fwk
; :: thesis: b_{1} in { (F . b_{2}) where w is Element of NAT : ( A <= b_{2} & b_{2} <= (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;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

suppose A14:
x in {(F . ((A + k) + 1))}
; :: thesis: b_{1} in { (F . b_{2}) where w is Element of NAT : ( A <= b_{2} & b_{2} <= (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;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

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

then
card (Fwk \/ {(F . ((A + k) + 1))}) = (k + 1) + 1
by A4, CARD_2:41;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 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

hence S

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 ) } ) )

then
{ (F . w) where w is Element of NAT : ( A <= w & w <= A + 0 ) } = {(F . A)}
by TARSKI:2;( ( 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 ) } ) )

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;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 . A)}
; :: thesis: 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;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

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

then A21: S

for k being Nat holds S

hence card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1 ; :: thesis: verum