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 S₁[ 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: S₁[ 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 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]
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) - (card {w}) by A6, CARD_2:44, ZFMISC_1:31
.= (k + 1) - 1 by A5, CARD_2:42 ;
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 A5, A6, FUNCT_2:11;
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 A6, XBOOLE_1:45, ZFMISC_1:31;
n0 < (n0 + n1) + 1 by NAT_1:11, NAT_1:13;
then x | (Segm n0) c= x | (Segm ((n0 + n1) + 1)) by NAT_1:39, RELAT_1:75;
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 NAT_1:11, NAT_1:13;
then ( n1 in Segm ((n0 + n1) + 1) & dom x = NAT ) by FUNCT_2:def 1, NAT_1:44;
then {w} c= rng (x | (Segm ((n0 + n1) + 1))) by A9, FUNCT_1:50, ZFMISC_1:31;
hence A c= rng (x | (Segm ((n0 + n1) + 1))) by A10, A11, XBOOLE_1:8; :: thesis: verum

end;

A12: for k being Nat holds S₁[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 A12, A13; :: thesis: verum