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

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng G or v in S )
assume v in rng G ; :: thesis: v in S
then consider k being object such that
A3: k in dom G and
A4: v = G . k by FUNCT_1:def 3;
A5: F . k in rng F by A1, A3, FUNCT_1:3;
G . k = (F . k) /\ A by A1, A2, A3;
hence v in S by A4, A5, FINSUB_1:def 2; :: thesis: verum

end;

then reconsider G = G as FinSequence of S by FINSEQ_1:def 4;

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
A6: i in dom G and
A7: j in dom G and
A8: i <> j ; :: thesis: G . i misses G . j
A9: F . i misses F . j by A8, PROB_2:def 2;
A10: G . j = (F . j) /\ A by A1, A2, A7;
G . i = (F . i) /\ A by A1, A2, A6;
hence G . i misses G . j by A10, A9, XBOOLE_1:76; :: thesis: verum

end;

hence G is Finite_Sep_Sequence of S by MESFUNC3:4; :: thesis: verum