let FT be non empty RelStr ; :: thesis: for f being FinSequence of FT

for A being Subset of FT

for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let f be FinSequence of FT; :: thesis: for A being Subset of FT

for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let x1, x2 be Element of FT; :: thesis: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 implies ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) ) )

defpred S_{1}[ Nat] means ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & $1 = len g );

assume ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; :: thesis: ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

then A1: ex k being Nat st S_{1}[k]
;

ex k being Nat st

( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A1);

then consider k0 being Nat such that

A2: S_{1}[k0]
and

A3: for n being Nat st S_{1}[n] holds

k0 <= n ;

consider g0 being FinSequence of FT such that

A4: ( g0 is continuous & rng g0 c= A & g0 . 1 = x1 & g0 . (len g0) = x2 ) and

A5: k0 = len g0 by A2;

for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g0 <= len h by A3, A5;

hence ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) ) by A4; :: thesis: verum

for A being Subset of FT

for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let f be FinSequence of FT; :: thesis: for A being Subset of FT

for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds

ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

let x1, x2 be Element of FT; :: thesis: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 implies ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) ) )

defpred S

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & $1 = len g );

assume ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; :: thesis: ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) )

then A1: ex k being Nat st S

ex k being Nat st

( S

k <= n ) ) from NAT_1:sch 5(A1);

then consider k0 being Nat such that

A2: S

A3: for n being Nat st S

k0 <= n ;

consider g0 being FinSequence of FT such that

A4: ( g0 is continuous & rng g0 c= A & g0 . 1 = x1 & g0 . (len g0) = x2 ) and

A5: k0 = len g0 by A2;

for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g0 <= len h by A3, A5;

hence ex g being FinSequence of FT st

( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds

len g <= len h ) ) by A4; :: thesis: verum