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

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

for n, m being Nat st n <= m holds

F . n c= G . m

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

for n, m being Nat st n <= m holds

F . n c= G . m

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

F . n c= G . m )

assume that

A1: G . 0 = N . 0 and

A2: for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) and

A3: F . 0 = N . 0 and

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

F . n c= G . m

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

A5: for n being Nat holds F . n c= G . n

then ( n = m or n < m ) by XXREAL_0:1;

hence F . n c= G . m by A5, A9; :: thesis: verum

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

for n, m being Nat st n <= m holds

F . n c= G . m

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

for n, m being Nat st n <= m holds

F . n c= G . m

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

F . n c= G . m )

assume that

A1: G . 0 = N . 0 and

A2: for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) and

A3: F . 0 = N . 0 and

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

F . n c= G . m

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

A5: for n being Nat holds F . n c= G . n

proof

A9:
( n < m implies F . n c= G . m )
defpred S_{1}[ Nat] means F . $1 c= G . $1;

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

S_{1}[n + 1]
_{1}[ 0 ]
by A1, A3;

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

end;A6: for n being Nat st S

S

proof

A8:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

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

G . (n + 1) = (N . (n + 1)) \/ (G . n) by A2;

then A7: N . (n + 1) c= G . (n + 1) by XBOOLE_1:7;

F . (n + 1) = (N . (n + 1)) \ (G . n) by A4;

hence S_{1}[n + 1]
by A7, XBOOLE_1:1; :: thesis: verum

end;assume F . n c= G . n ; :: thesis: S

G . (n + 1) = (N . (n + 1)) \/ (G . n) by A2;

then A7: N . (n + 1) c= G . (n + 1) by XBOOLE_1:7;

F . (n + 1) = (N . (n + 1)) \ (G . n) by A4;

hence S

thus for n being Nat holds S

proof

assume
n <= m
; :: thesis: F . n c= G . m
assume
n < m
; :: thesis: F . n c= G . m

then A10: G . n c= G . m by A1, A2, Th6;

F . n c= G . n by A5;

hence F . n c= G . m by A10; :: thesis: verum

end;then A10: G . n c= G . m by A1, A2, Th6;

F . n c= G . n by A5;

hence F . n c= G . m by A10; :: thesis: verum

then ( n = m or n < m ) by XXREAL_0:1;

hence F . n c= G . m by A5, A9; :: thesis: verum