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

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

then reconsider G = G as FinSequence of S by FINSEQ_1:def 4;
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;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

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

G . i misses G . j

hence
G is Finite_Sep_Sequence of S
by MESFUNC3:4; :: thesis: verumG . 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;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