let X be non empty set ; :: thesis: for seq being sequence of X
for f being FinSequence of X st rng f c= rng seq holds
ex N being Nat st rng f c= rng (seq | (Segm N))
let seq be sequence of X; :: thesis: for f being FinSequence of X st rng f c= rng seq holds
ex N being Nat st rng f c= rng (seq | (Segm N))
let f be FinSequence of X; :: thesis: ( rng f c= rng seq implies ex N being Nat st rng f c= rng (seq | (Segm N)) )
assume A1: rng f c= rng seq ; :: thesis: ex N being Nat st rng f c= rng (seq | (Segm N))
defpred S₁[ Nat] means for F being FinSequence of X st len F = $1 & rng F c= rng seq holds
ex N being Nat st rng F c= rng (seq | (Segm N));

now :: thesis: for F being FinSequence of X st len F = 0 & rng F c= rng seq holds
ex N being Nat st rng F c= rng (seq | (Segm N))

let F be FinSequence of X; :: thesis: ( len F = 0 & rng F c= rng seq implies ex N being Nat st rng F c= rng (seq | (Segm N)) )
assume ( len F = 0 & rng F c= rng seq ) ; :: thesis: ex N being Nat st rng F c= rng (seq | (Segm N))
then F = {} ;
then rng F c= rng (seq | (Segm 0)) ;
hence ex N being Nat st rng F c= rng (seq | (Segm N)) ; :: thesis: verum

end;

then A2: S₁[ 0 ] ;
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]

now :: thesis: for F being FinSequence of X st len F = k + 1 & rng F c= rng seq holds
ex N being Nat st rng F c= rng (seq | (Segm N))

let F be FinSequence of X; :: thesis: ( len F = k + 1 & rng F c= rng seq implies ex N being Nat st rng N c= rng (seq | (Segm b₂)) )
assume that
A5: len F = k + 1 and
A6: rng F c= rng seq ; :: thesis: ex N being Nat st rng N c= rng (seq | (Segm b₂))
reconsider F1 = F | k as FinSequence of X ;
k <= len F by A5, NAT_1:13;
then A7: len F1 = k by FINSEQ_1:59;
A8: F1 = F | (Seg k) by FINSEQ_1:def 16;
rng (F | (Seg k)) c= rng F by RELAT_1:70;
then rng F1 c= rng seq by A6, A8;
then consider N1 being Nat such that
A9: rng F1 c= rng (seq | (Segm N1)) by A4, A7;
1 <= k + 1 by NAT_1:11;
then k + 1 in dom F by A5, FINSEQ_3:25;
then F . (k + 1) in rng F by FUNCT_1:3;
then consider m being Element of NAT such that
A10: F . (k + 1) = seq . m by A6, FUNCT_2:113;
reconsider m = m as Nat ;
F = F1 ^ <*(F . (k + 1))*> by A5, A8, FINSEQ_3:55;
then rng F = (rng F1) \/ (rng <*(F . (k + 1))*>) by FINSEQ_1:31;
then A11: rng F = (rng F1) \/ {(F . (k + 1))} by FINSEQ_1:38;
A12: dom seq = NAT by FUNCT_2:def 1;

per cases ( m < N1 or m >= N1 ) ;

suppose A13: m < N1 ; :: thesis: ex N being Nat st rng N c= rng (seq | (Segm b₂))

then m in Segm N1 by NAT_1:44;
then m in (dom seq) /\ (Segm N1) by A12, XBOOLE_0:def 4;
then m in dom (seq | (Segm N1)) by RELAT_1:61;
then (seq | (Segm N1)) . m in rng (seq | (Segm N1)) by FUNCT_1:3;
then F . (k + 1) in rng (seq | (Segm N1)) by A10, A13, FUNCT_1:49, NAT_1:44;
then {(F . (k + 1))} c= rng (seq | (Segm N1)) by TARSKI:def 1;
hence ex N being Nat st rng F c= rng (seq | (Segm N)) by A9, A11, XBOOLE_1:8; :: thesis: verum

end;

suppose m >= N1 ; :: thesis: ex N being Nat st rng N c= rng (seq | (Segm b₂))

then m + 1 > N1 by NAT_1:13;
then seq | (Segm N1) c= seq | (Segm (m + 1)) by RELAT_1:75, NAT_1:39;
then rng (seq | (Segm N1)) c= rng (seq | (Segm (m + 1))) by RELAT_1:11;
then A14: rng F1 c= rng (seq | (Segm (m + 1))) by A9;
A15: m < m + 1 by NAT_1:13;
then m in Segm (m + 1) by NAT_1:44;
then m in (dom seq) /\ (Segm (m + 1)) by A12, XBOOLE_0:def 4;
then m in dom (seq | (Segm (m + 1))) by RELAT_1:61;
then (seq | (Segm (m + 1))) . m in rng (seq | (Segm (m + 1))) by FUNCT_1:3;
then F . (k + 1) in rng (seq | (Segm (m + 1))) by A10, A15, NAT_1:44, FUNCT_1:49;
then {(F . (k + 1))} c= rng (seq | (Segm (m + 1))) by TARSKI:def 1;
hence ex N being Nat st rng F c= rng (seq | (Segm N)) by A11, A14, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
then S₁[ len f] ;
hence ex N being Nat st rng f c= rng (seq | (Segm N)) by A1; :: thesis: verum