let R be non empty doubleLoopStr ; :: thesis: ( ( for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal ) ) implies for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal )
assume A1: for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal ) ; :: thesis: for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal
let a be sequence of R; :: thesis: ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal
reconsider B = rng a as non empty Subset of R ;
consider C being non empty finite Subset of R such that
A2: C c= B and
A3: C -Ideal = B -Ideal by A1;
defpred S₁[ object , object ] means $1 = a . $2;
A4: dom a = NAT by FUNCT_2:def 1;
A5: for e being object st e in C holds
ex u being object st
( u in NAT & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in C implies ex u being object st
( u in NAT & S₁[e,u] ) )
assume e in C ; :: thesis: ex u being object st
( u in NAT & S₁[e,u] )
then consider u being object such that
A6: u in dom a and
A7: e = a . u by A2, FUNCT_1:def 3;
take u ; :: thesis: ( u in NAT & S₁[e,u] )
thus u in NAT by A6; :: thesis: S₁[e,u]
thus S₁[e,u] by A7; :: thesis: verum

end;

consider f being Function of C,NAT such that
A8: for e being object st e in C holds
S₁[e,f . e] from FUNCT_2:sch 1(A5);
set Rf = rng f;
reconsider Rf = rng f as non empty finite Subset of NAT ;
reconsider m = max Rf as Element of NAT by ORDINAL1:def 12;
set D = rng (a | (Segm (m + 1)));
A9: dom f = C by FUNCT_2:def 1;
A10: C c= rng (a | (Segm (m + 1)))

proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in C or X in rng (a | (Segm (m + 1))) )
set fx = f . X;
assume A11: X in C ; :: thesis: X in rng (a | (Segm (m + 1)))
then f . X in Rf by A9, FUNCT_1:def 3;
then f . X <= m by XXREAL_2:def 8;
then f . X < m + 1 by NAT_1:13;
then f . X in Segm (m + 1) by NAT_1:44;
then a . (f . X) in rng (a | (Segm (m + 1))) by A4, FUNCT_1:50;
hence X in rng (a | (Segm (m + 1))) by A8, A11; :: thesis: verum

end;

then reconsider D = rng (a | (Segm (m + 1))) as non empty Subset of R ;
A12: D -Ideal c= B -Ideal by Th57, RELAT_1:70;
B -Ideal c= D -Ideal by A3, A10, Th57;
then A13: D -Ideal = B -Ideal by A12;
take m ; :: thesis: a . (m + 1) in (rng (a | (m + 1))) -Ideal
( B c= B -Ideal & a . (m + 1) in B ) by Def14, FUNCT_2:4;
hence a . (m + 1) in (rng (a | (m + 1))) -Ideal by A13; :: thesis: verum