let X be RealLinearSpace; :: thesis: for x being sequence of X
for A being finite Subset of X st A c= rng x holds
ex n being Nat st A c= rng (x | (Segm n))

let x be sequence of X; :: thesis: for A being finite Subset of X st A c= rng x holds
ex n being Nat st A c= rng (x | (Segm n))

defpred S1[ Nat] means for A being finite Subset of X st card A = \$1 & A c= rng x holds
ex n being Nat st A c= rng (x | (Segm n));
A1: S1[ 0 ]
proof
let A be finite Subset of the carrier of X; :: thesis: ( card A = 0 & A c= rng x implies ex n being Nat st A c= rng (x | (Segm n)) )
assume A2: ( card A = 0 & A c= rng x ) ; :: thesis: ex n being Nat st A c= rng (x | (Segm n))
set n = the Nat;
take the Nat ; :: thesis: A c= rng (x | (Segm the Nat))
thus A c= rng (x | (Segm the Nat)) by A2; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let A be finite Subset of the carrier of X; :: thesis: ( card A = k + 1 & A c= rng x implies ex n being Nat st A c= rng (x | (Segm n)) )
assume A5: ( card A = k + 1 & A c= rng x ) ; :: thesis: ex n being Nat st A c= rng (x | (Segm n))
then A <> {} ;
then consider w being object such that
A6: w in A by XBOOLE_0:def 1;
reconsider w = w as Element of the carrier of X by A6;
A7: card (A \ {w}) = (card A) - () by
.= (k + 1) - 1 by ;
reconsider A0 = A \ {w} as finite Subset of X ;
A0 c= A by XBOOLE_1:36;
then A0 c= rng x by A5;
then consider n0 being Nat such that
A8: A0 c= rng (x | (Segm n0)) by A4, A7;
consider n1 being object such that
A9: ( n1 in NAT & w = x . n1 ) by ;
reconsider n1 = n1 as Nat by A9;
set n = (n0 + n1) + 1;
take (n0 + n1) + 1 ; :: thesis: A c= rng (x | (Segm ((n0 + n1) + 1)))
A10: A = A0 \/ {w} by ;
n0 < (n0 + n1) + 1 by ;
then x | (Segm n0) c= x | (Segm ((n0 + n1) + 1)) by ;
then rng (x | (Segm n0)) c= rng (x | (Segm ((n0 + n1) + 1))) by RELAT_1:11;
then A11: A0 c= rng (x | (Segm ((n0 + n1) + 1))) by A8;
n1 < (n0 + n1) + 1 by ;
then ( n1 in Segm ((n0 + n1) + 1) & dom x = NAT ) by ;
then {w} c= rng (x | (Segm ((n0 + n1) + 1))) by ;
hence A c= rng (x | (Segm ((n0 + n1) + 1))) by ; :: thesis: verum
end;
A12: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A3);
let A be finite Subset of the carrier of X; :: thesis: ( A c= rng x implies ex n being Nat st A c= rng (x | (Segm n)) )
assume A13: A c= rng x ; :: thesis: ex n being Nat st A c= rng (x | (Segm n))
card A is Nat ;
hence ex n being Nat st A c= rng (x | (Segm n)) by ; :: thesis: verum