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 & C -Ideal = B -Ideal ) by A1;
defpred S₁[ set , set ] means $1 = a . $2;
A3: dom a = NAT by FUNCT_2:def 1;
A4: for e being set st e in C holds
ex u being set st
( u in NAT & S₁[e,u] )

proof

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

end;

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

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in C or X in rng (a | (Segm (m + 1))) )
assume A9: X in C ; :: thesis: X in rng (a | (Segm (m + 1)))
then A10: f . X in Rf by A7, FUNCT_1:def 5;
set fx = f . X;
f . X <= m by A10, XXREAL_2:def 8;
then f . X < m + 1 by NAT_1:13;
then f . X in Segm (m + 1) by GR_CY_1:10;
then a . (f . X) in rng (a | (Segm (m + 1))) by A3, FUNCT_1:73;
hence X in rng (a | (Segm (m + 1))) by A6, A9; :: thesis: verum

end;

then reconsider D = rng (a | (Segm (m + 1))) as non empty Subset of R ;
A11: B -Ideal c= D -Ideal by A2, A8, Th57;
D -Ideal c= B -Ideal by Th57, RELAT_1:99;
then A12: D -Ideal = B -Ideal by A11, XBOOLE_0:def 10;
A13: B c= B -Ideal by Def15;
a . (m + 1) in B by FUNCT_2:6;
hence a . (m + 1) in (rng (a | (m + 1))) -Ideal by A12, A13; :: thesis: verum