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

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

hence
F is Sep_Sequence of S
by PROB_2:def 2; :: thesis: verum
let n, m be object ; :: thesis: ( n <> m implies F . n misses F . m )

assume A2: n <> m ; :: thesis: F . n misses F . m

end;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 )
;

end;