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 n, m being Nat st n < m holds

F . n c= F . m

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 n, m being Nat st n < m holds

F . n c= F . m

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 n, m being Nat st n < m holds

F . n c= F . m )

assume that

A1: F . 0 = N . 0 and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for n, m being Nat st n < m holds

F . n c= F . m

defpred S_{1}[ Nat] means for m being Nat st $1 < m holds

F . $1 c= F . m;

A3: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A3, A11); :: 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 n, m being Nat st n < m holds

F . n c= F . m

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 n, m being Nat st n < m holds

F . n c= F . m

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 n, m being Nat st n < m holds

F . n c= F . m )

assume that

A1: F . 0 = N . 0 and

A2: for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; :: thesis: for n, m being Nat st n < m holds

F . n c= F . m

defpred S

F . $1 c= F . m;

A3: S

proof

A11:
for n being Nat st S
A4:
for k being Nat st 0 < k + 1 holds

F . 0 c= F . (k + 1)

assume A9: 0 < m ; :: thesis: F . 0 c= F . m

then consider k being Nat such that

A10: m = k + 1 by NAT_1:6;

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

m = k + 1 by A10;

hence F . 0 c= F . m by A9, A4; :: thesis: verum

end;F . 0 c= F . (k + 1)

proof

let m be Nat; :: thesis: ( 0 < m implies F . 0 c= F . m )
defpred S_{2}[ Nat] means ( 0 < $1 + 1 implies F . 0 c= F . ($1 + 1) );

A5: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

then A8: S_{2}[ 0 ]
by XBOOLE_1:7;

thus for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A8, A5); :: thesis: verum

end;A5: for k being Nat st S

S

proof

F . (0 + 1) = (N . (0 + 1)) \/ (F . 0)
by A2;
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

A6: 0 <= k by NAT_1:2;

F . ((k + 1) + 1) = (N . ((k + 1) + 1)) \/ (F . (k + 1)) by A2;

then A7: F . (k + 1) c= F . ((k + 1) + 1) by XBOOLE_1:7;

assume ( 0 < k + 1 implies F . 0 c= F . (k + 1) ) ; :: thesis: S_{2}[k + 1]

hence S_{2}[k + 1]
by A7, A6, NAT_1:13, XBOOLE_1:1; :: thesis: verum

end;A6: 0 <= k by NAT_1:2;

F . ((k + 1) + 1) = (N . ((k + 1) + 1)) \/ (F . (k + 1)) by A2;

then A7: F . (k + 1) c= F . ((k + 1) + 1) by XBOOLE_1:7;

assume ( 0 < k + 1 implies F . 0 c= F . (k + 1) ) ; :: thesis: S

hence S

then A8: S

thus for k being Nat holds S

assume A9: 0 < m ; :: thesis: F . 0 c= F . m

then consider k being Nat such that

A10: m = k + 1 by NAT_1:6;

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

m = k + 1 by A10;

hence F . 0 c= F . m by A9, A4; :: thesis: verum

S

proof

thus
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A12: for m being Nat st n < m holds

F . n c= F . m ; :: thesis: S_{1}[n + 1]

let m be Nat; :: thesis: ( n + 1 < m implies F . (n + 1) c= F . m )

assume A13: n + 1 < m ; :: thesis: F . (n + 1) c= F . m

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in F . (n + 1) or r in F . m )

A14: ( r in F . n implies r in F . m )

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

( r in N . (n + 1) implies r in F . m ) by A1, A2, A13, Th5;

hence r in F . m by A16, A17, A14, XBOOLE_0:def 3; :: thesis: verum

end;assume A12: for m being Nat st n < m holds

F . n c= F . m ; :: thesis: S

let m be Nat; :: thesis: ( n + 1 < m implies F . (n + 1) c= F . m )

assume A13: n + 1 < m ; :: thesis: F . (n + 1) c= F . m

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in F . (n + 1) or r in F . m )

A14: ( r in F . n implies r in F . m )

proof

assume A16:
r in F . (n + 1)
; :: thesis: r in F . m
assume A15:
r in F . n
; :: thesis: r in F . m

( n < m implies r in F . m )

end;( n < m implies r in F . m )

proof

hence
r in F . m
by A13, NAT_1:13; :: thesis: verum
assume
n < m
; :: thesis: r in F . m

then F . n c= F . m by A12;

hence r in F . m by A15; :: thesis: verum

end;then F . n c= F . m by A12;

hence r in F . m by A15; :: thesis: verum

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

( r in N . (n + 1) implies r in F . m ) by A1, A2, A13, Th5;

hence r in F . m by A16, A17, A14, XBOOLE_0:def 3; :: thesis: verum