let M be non empty set ; :: thesis: for x being sequence of M st rng x is finite holds
ex z being Element of M st
( x " {z} c= NAT & x " {z} is infinite )
let x be sequence of M; :: thesis: ( rng x is finite implies ex z being Element of M st
( x " {z} c= NAT & x " {z} is infinite ) )
assume A1: rng x is finite ; :: thesis: ex z being Element of M st
( x " {z} c= NAT & x " {z} is infinite )
assume A2: for z being Element of M holds
( not x " {z} c= NAT or not x " {z} is infinite ) ; :: thesis: contradiction
deffunc H1( object ) -> Element of K19(NAT) = x " {$1};
set K = { H1(w) where w is Element of M : w in rng x } ;
A3: { H1(w) where w is Element of M : w in rng x } is finite from FRAENKEL:sch 21(A1);
 for Y being set st Y in { H1(w) where w is Element of M : w in rng x } holds
Y is finite
proof
let Y be set ; :: thesis: ( Y in { H1(w) where w is Element of M : w in rng x } implies Y is finite )
assume Y in { H1(w) where w is Element of M : w in rng x } ; :: thesis: Y is finite
then consider w being Element of M such that
A4: ( Y = x " {w} & w in rng x ) ;
thus Y is finite by A2, A4; :: thesis: verum
end;
then A5: union { H1(w) where w is Element of M : w in rng x } is finite by A3, FINSET_1:7;
dom x c= union { H1(w) where w is Element of M : w in rng x }
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in dom x or s in union { H1(w) where w is Element of M : w in rng x } )
assume A6: s in dom x ; :: thesis: s in union { H1(w) where w is Element of M : w in rng x }
then reconsider sn = s as Element of NAT ;
reconsider w = x . sn as Element of M ;
w in rng x by A6, FUNCT_1:3;
then A7: x " {w} in { H1(w) where w is Element of M : w in rng x } ;
w in {w} by TARSKI:def 1;
then s in x " {w} by A6, FUNCT_1:def 7;
hence s in union { H1(w) where w is Element of M : w in rng x } by A7, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A5, FUNCT_2:def 1; :: thesis: verum