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₁[ 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₁[k] ;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A1);
then consider k0 being Nat such that
A2: S₁[k0] and
A3: for n being Nat st S₁[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