let R be non empty doubleLoopStr ; :: thesis: ( ( for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal ) implies for F being Function of NAT ,(bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) ) )
assume A1: for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal ; :: thesis: for F being Function of NAT ,(bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) )
given F being Function of NAT ,(bool the carrier of R) such that A2: for i being Element of NAT holds F . i is Ideal of R and
A3: for j, k being Element of NAT st j < k holds
F . j c< F . k ; :: thesis: contradiction
defpred S1[ set , set ] means ex n being Element of NAT st
( n = $1 & ( n = 0 implies $2 in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & $2 in (F . n) \ (F . k) ) ) );
A4: for e being set st e in NAT holds
ex u being set st
( u in the carrier of R & S1[e,u] )
proof
let e be set ; :: thesis: ( e in NAT implies ex u being set st
( u in the carrier of R & S1[e,u] ) )
assume A5: e in NAT ; :: thesis: ex u being set st
( u in the carrier of R & S1[e,u] )
reconsider n = e as Element of NAT by A5;
per cases ( n = 0 or n > 0 ) ;
suppose A6: n = 0 ; :: thesis: ex u being set st
( u in the carrier of R & S1[e,u] )
F . 0 is Ideal of R by A2;
then consider u being set such that
A7: u in F . 0 by XBOOLE_0:def 1;
take u ; :: thesis: ( u in the carrier of R & S1[e,u] )
thus u in the carrier of R by A7; :: thesis: S1[e,u]
take n ; :: thesis: ( n = e & ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus n = e ; :: thesis: ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) ) by A6, A7; :: thesis: verum
end;
suppose n > 0 ; :: thesis: ex u being set st
( u in the carrier of R & S1[e,u] )
then consider k being Nat such that
A8: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n > k by A8, NAT_1:13;
then not F . n c= F . k by A3, XBOOLE_1:60;
then not (F . n) \ (F . k) is empty by XBOOLE_1:37;
then consider u being set such that
A9: u in (F . n) \ (F . k) by XBOOLE_0:def 1;
take u ; :: thesis: ( u in the carrier of R & S1[e,u] )
thus u in the carrier of R by A9; :: thesis: S1[e,u]
take n ; :: thesis: ( n = e & ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus n = e ; :: thesis: ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) ) by A8, A9; :: thesis: verum
end;
end;
end;
consider f being Function of NAT ,the carrier of R such that
A10: for e being set st e in NAT holds
S1[e,f . e] from FUNCT_2:sch 1(A4);
 defpred S2[ Element of NAT ] means rng (f | (Segm ($1 + 1))) c= F . $1;
A11: S2[ 0 ]
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (Segm (0 + 1))) or y in F . 0 )
assume y in rng (f | (Segm (0 + 1))) ; :: thesis: y in F . 0
then consider x being set such that
A12: x in dom (f | (Segm 1)) and
A13: y = (f | (Segm 1)) . x by FUNCT_1:def 5;
A14: ( x in Segm 1 & x in dom f ) by A12, RELAT_1:86;
ex n being Element of NAT st
( n = x & ( n = 0 implies f . x in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . x in (F . n) \ (F . k) ) ) ) by A10, A12;
hence y in F . 0 by A13, A14, FUNCT_1:72, GR_CY_1:13, TARSKI:def 1; :: thesis: verum
end;
A15: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A16: rng (f | (Segm (k + 1))) c= F . k ; :: thesis: S2[k + 1]
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (Segm ((k + 1) + 1))) or y in F . (k + 1) )
assume A17: y in rng (f | (Segm ((k + 1) + 1))) ; :: thesis: y in F . (k + 1)
consider x being set such that
A18: x in dom (f | (Segm ((k + 1) + 1))) and
A19: y = (f | (Segm ((k + 1) + 1))) . x by A17, FUNCT_1:def 5;
A20: ( x in Segm ((k + 1) + 1) & x in dom f ) by A18, RELAT_1:86;
reconsider nx = x as Element of NAT by A18;
nx < (k + 1) + 1 by A20, GR_CY_1:10;
then A21: nx <= k + 1 by NAT_1:13;
per cases ( nx < k + 1 or nx = k + 1 ) by A21, XXREAL_0:1;
suppose nx < k + 1 ; :: thesis: y in F . (k + 1)
then A22: nx in Segm (k + 1) by GR_CY_1:10;
y = f . nx by A18, A19, FUNCT_1:70;
then y in rng (f | (Segm (k + 1))) by A20, A22, FUNCT_1:73;
then A23: y in F . k by A16;
k < k + 1 by NAT_1:13;
then F . k c< F . (k + 1) by A3;
then F . k c= F . (k + 1) by XBOOLE_0:def 8;
hence y in F . (k + 1) by A23; :: thesis: verum
end;
suppose A24: nx = k + 1 ; :: thesis: y in F . (k + 1)
A25: y = f . nx by A18, A19, FUNCT_1:70;
consider n being Element of NAT such that
A26: n = nx and
( n = 0 implies f . nx in F . 0 ) and
A27: ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . nx in (F . n) \ (F . k) ) ) by A10;
consider m being Element of NAT such that
A28: ( n = m + 1 & f . nx in (F . n) \ (F . m) ) by A24, A26, A27;
thus y in F . (k + 1) by A24, A25, A26, A28, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
A29: for m being Element of NAT holds S2[m] from NAT_1:sch 1(A11, A15);
 consider m being Element of NAT such that
A30: f . (m + 1) in (rng (f | (m + 1))) -Ideal by A1;
F . m is Ideal of R by A2;
then A31: F . m = (F . m) -Ideal by Th44;
reconsider m1 = m + 1 as non zero natural number ;
A32: (rng (f | (Segm m1))) -Ideal c= F . m by A29, A31, Th57;
consider n being Element of NAT such that
A33: n = m + 1 and
( n = 0 implies f . (m + 1) in F . 0 ) and
A34: ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . (m + 1) in (F . n) \ (F . k) ) ) by A10;
consider k being Element of NAT such that
A35: n = k + 1 and
A36: f . (m + 1) in (F . n) \ (F . k) by A33, A34;
thus contradiction by A30, A32, A33, A35, A36, XBOOLE_0:def 5; :: thesis: verum