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_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

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

ex n being Nat st A c= rng (x | (Segm n));

A1: S

proof

A3:
for k being Nat st S
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;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

S

proof

A12:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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;assume A4: S

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

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