let X be set ; :: thesis: for S being non empty Subset-Family of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let S be non empty Subset-Family of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) ) )

assume that

A1: F . 0 = N . 0 and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let r be set ; :: thesis: for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let n be Nat; :: thesis: ( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

defpred S_{1}[ Nat] means ( ex k being Nat st

( k <= $1 & r in N . k ) implies r in F . $1 );

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

( k <= n & r in N . k ) ) :: thesis: ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n )_{1}[ 0 ]
by A1, NAT_1:3;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A16, A3);

hence ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: verum

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let S be non empty Subset-Family of X; :: thesis: for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let N, F be sequence of S; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) ) )

assume that

A1: F . 0 = N . 0 and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let r be set ; :: thesis: for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

let n be Nat; :: thesis: ( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

defpred S

( k <= $1 & r in N . k ) implies r in F . $1 );

A3: for n being Nat st S

S

proof

thus
( r in F . n implies ex k being Nat st
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: S_{1}[n + 1]

A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;

given k being 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;assume A4: ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: S

A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2;

given k being 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

( k <= n & r in N . k ) ) :: thesis: ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n )

proof

A16:
S
defpred S_{2}[ Nat] means r in F . $1;

assume A8: r in F . n ; :: thesis: ex k being Nat st

( k <= n & r in N . k )

then A9: ex n being Nat st S_{2}[n]
;

ex s being Nat st

( S_{2}[s] & ( for k being Nat st S_{2}[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 ) )

( k <= n & r in N . k ) ) by A1, A10, NAT_1:2;

hence ex k being Nat st

( k <= n & r in N . k ) by A12, NAT_1:6; :: thesis: verum

end;assume A8: r in F . n ; :: thesis: ex k being Nat st

( k <= n & r in N . k )

then A9: ex n being Nat st S

ex s being Nat st

( S

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

( s = 0 implies ex k being Element of NAT st
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

A15: s in NAT by ORDINAL1:def 12;

F . s = (N . s) \/ (F . k) by A2, A13;

hence ( s is Element of NAT & s <= n & r in N . s ) by A8, A10, A11, A14, A15, XBOOLE_0:def 3; :: thesis: verum

end;( k <= n & r in N . k )

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A14: not r in F . k

proof

take
s
; :: thesis: ( s is Element of NAT & s <= n & r in N . s )
assume
r in F . k
; :: thesis: contradiction

then s <= k by A11;

hence contradiction by A13, NAT_1:13; :: thesis: verum

end;then s <= k by A11;

hence contradiction by A13, NAT_1:13; :: thesis: verum

A15: s in NAT by ORDINAL1:def 12;

F . s = (N . s) \/ (F . k) by A2, A13;

hence ( s is Element of NAT & s <= n & r in N . s ) by A8, A10, A11, A14, A15, XBOOLE_0:def 3; :: thesis: verum

( k <= n & r in N . k ) ) by A1, A10, NAT_1:2;

hence ex k being Nat st

( k <= n & r in N . k ) by A12, NAT_1:6; :: thesis: verum

for n being Nat holds S

hence ( ex k being Nat st

( k <= n & r in N . k ) implies r in F . n ) ; :: thesis: verum