let X be set ; :: thesis: for S being non empty Subset-Family of X
for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let S be non empty Subset-Family of X; :: thesis: for N, F being Function of NAT,S st F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds
for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let N, F be Function of NAT,S; :: thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) ) )
assume that
A1: F . 0 = N . 0 and
A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for r being set
for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let r be set ; :: thesis: for n being Element of NAT holds
( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
let n be Element of NAT ; :: thesis: ( r in F . n iff ex k being Element of NAT st
( k <= n & r in N . k ) )
defpred S₁[ Element of NAT ] means ( ex k being Element of NAT st
( k <= $1 & r in N . k ) implies r in F . $1 );
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: S₁[n + 1]
A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;
given k being Element of NAT such that A6: k <= n + 1 and
A7: r in N . k ; :: thesis: r in F . (n + 1)
( k <= n or k = n + 1 ) by A6, NAT_1:8;
hence r in F . (n + 1) by A4, A7, A5, XBOOLE_0:def 3; :: thesis: verum

end;

thus ( r in F . n implies ex k being Element of NAT st
( k <= n & r in N . k ) ) :: thesis: ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n )

proof

defpred S₂[ Nat] means r in F . $1;
assume A8: r in F . n ; :: thesis: ex k being Element of NAT st
( k <= n & r in N . k )
then A9: ex n being Nat st S₂[n] ;
ex s being Nat st
( S₂[s] & ( for k being Nat st S₂[k] holds
s <= k ) ) from NAT_1:sch 5(A9);
then consider s being Nat such that
A10: r in F . s and
A11: for k being Nat st r in F . k holds
s <= k ;
A12: ( ex k being Nat st s = k + 1 implies ex k being Element of NAT st
( k <= n & r in N . k ) )

proof

given k being Nat such that A13: s = k + 1 ; :: thesis: ex k being Element of NAT st
( k <= n & r in N . k )
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A14: not r in F . k

proof

assume r in F . k ; :: thesis: contradiction
then s <= k by A11;
hence contradiction by A13, NAT_1:13; :: thesis: verum

end;

take s ; :: thesis: ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s )
A15: s in NAT by ORDINAL1:def 12;
F . s = (N . s) \/ (F . k) by A2, A13;
hence ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s ) by A8, A10, A11, A14, A15, XBOOLE_0:def 3; :: thesis: verum

end;

( s = 0 implies ex k being Element of NAT st
( k <= n & r in N . k ) ) by A1, A10, NAT_1:2;
hence ex k being Element of NAT st
( k <= n & r in N . k ) by A12, NAT_1:6; :: thesis: verum

end;

A16: S₁[ 0 ] by A1, NAT_1:3;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A16, A3);
hence ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: verum