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 A1, Th19;
( n9 < m9 implies F . n misses F . m ) by A1, Th19;
hence F . n misses F . m by A2, A3, XXREAL_0:1; :: 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