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 set ; :: 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 set such that
A3: ( k in dom G & v = G . k ) by FUNCT_1:def 5;
A4: G . k = (F . k) /\ A by A1, A2, A3;
F . k in rng F by A1, A3, FUNCT_1:12;
hence v in S by A3, A4, FINSUB_1:def 2; :: thesis: verum

end;

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

now

let i, j be Nat; :: thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume A5: ( i in dom G & j in dom G & i <> j ) ; :: thesis: G . i misses G . j
then A6: ( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A1, A2;
F . i misses F . j by A5, PROB_2:def 3;
hence G . i misses G . j by A6, XBOOLE_1:76; :: thesis: verum

end;

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