let X be non empty set ; :: thesis: for A being set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let A be set ; :: thesis: for S being SigmaField of X
for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let S be SigmaField of X; :: thesis: for F being Finite_Sep_Sequence of S
for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let F be Finite_Sep_Sequence of S; :: thesis: for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
let G be FinSequence of S; :: thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) implies G is Finite_Sep_Sequence of S )
assume that
A1: dom G = dom F and
A2: for i being Nat st i in dom G holds
G . i = A /\ (F . i) ; :: thesis: G is Finite_Sep_Sequence of S

now :: thesis: for i, j being Nat st i in dom G & j in dom G & i <> j holds
G . i misses G . j

let i, j be Nat; :: thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume that
A3: i in dom G and
A4: j in dom G and
A5: i <> j ; :: thesis: G . i misses G . j
A6: F . i misses F . j by A1, A3, A4, A5, Th4;
(A /\ (F . i)) /\ (A /\ (F . j)) = A /\ ((F . i) /\ (A /\ (F . j))) by XBOOLE_1:16
.= A /\ (((F . i) /\ (F . j)) /\ A) by XBOOLE_1:16
.= A /\ ({} /\ A) by A6
.= {} ;
then A /\ (F . i) misses A /\ (F . j) ;
then G . i misses A /\ (F . j) by A2, A3;
hence G . i misses G . j by A2, A4; :: thesis: verum

end;

hence G is Finite_Sep_Sequence of S by Th4; :: thesis: verum