let X be set ; :: thesis: for S being SigmaField 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)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S

let S be SigmaField 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)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S

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

assume A1: ( F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) ) ; :: thesis: F is Sep_Sequence of S
for n, m being object st n <> m holds
F . n misses F . m
proof
let n, m be object ; :: thesis: ( n <> m implies F . n misses F . m )
assume A2: n <> m ; :: thesis: F . n misses F . m
per cases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ;
suppose ( n in dom F & m in dom F ) ; :: thesis: F . n misses F . m
then reconsider n9 = n, m9 = m as Element of NAT ;
A3: ( m9 < n9 implies F . m misses F . n ) by ;
( n9 < m9 implies F . n misses F . m ) by ;
hence F . n misses F . m by ; :: thesis: verum
end;
suppose ( not n in dom F or not m in dom F ) ; :: thesis: F . n misses F . m
then ( F . n = {} or F . m = {} ) by FUNCT_1:def 2;
hence F . n misses F . m ; :: thesis: verum
end;
end;
end;
hence F is Sep_Sequence of S by PROB_2:def 2; :: thesis: verum