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 A1: ( F . 0 = N . 0 & ( 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 ) )
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 A2: r in F . n ; :: thesis: ex k being Element of NAT st
( k <= n & r in N . k )
then A3: 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(A3);
then consider s being Nat such that
A4: ( r in F . s & ( for k being Nat st r in F . k holds
s <= k ) ) ;
A5: ( s = 0 implies ex k being Element of NAT st
( k <= n & r in N . k ) )

proof

assume A6: s = 0 ; :: thesis: ex k being Element of NAT st
( k <= n & r in N . k )
take 0 ; :: thesis: ( 0 <= n & r in N . 0 )
thus ( 0 <= n & r in N . 0 ) by A1, A4, A6, NAT_1:2; :: thesis: verum

end;

( 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 A7: 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 13;
A8: F . s = (N . s) \/ (F . k) by A1, A7;
A9: not r in F . k

proof

assume r in F . k ; :: thesis: contradiction
then s <= k by A4;
hence contradiction by A7, 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 )
s in NAT by ORDINAL1:def 13;
hence ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s ) by A2, A4, A8, A9, XBOOLE_0:def 3; :: thesis: verum

end;

hence ex k being Element of NAT st
( k <= n & r in N . k ) by A5, NAT_1:6; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means ( ex k being Element of NAT st
( k <= $1 & r in N . k ) implies r in F . $1 );
A10: S₁[ 0 ] by A1, NAT_1:3;
A11: 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 A12: ( ex k being Element of NAT st
( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: S₁[n + 1]
given k being Element of NAT such that A13: ( k <= n + 1 & r in N . k ) ; :: thesis: r in F . (n + 1)
A14: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A1;
( k <= n or k = n + 1 ) by A13, NAT_1:8;
hence r in F . (n + 1) by A12, A13, A14, XBOOLE_0:def 3; :: thesis: verum

end;

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