let X be non empty set ; :: thesis: for S being SigmaField of X

for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let S be SigmaField of X; :: thesis: for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let n be Nat; :: thesis: for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let F be Relation; :: thesis: ( F is Finite_Sep_Sequence of S implies F | (Seg n) is Finite_Sep_Sequence of S )

assume A1: F is Finite_Sep_Sequence of S ; :: thesis: F | (Seg n) is Finite_Sep_Sequence of S

then reconsider G = F | (Seg n) as FinSequence of S by FINSEQ_1:18;

reconsider F = F as FinSequence of S by A1;

for k, m being object st k <> m holds

G . k misses G . m

for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let S be SigmaField of X; :: thesis: for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let n be Nat; :: thesis: for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

let F be Relation; :: thesis: ( F is Finite_Sep_Sequence of S implies F | (Seg n) is Finite_Sep_Sequence of S )

assume A1: F is Finite_Sep_Sequence of S ; :: thesis: F | (Seg n) is Finite_Sep_Sequence of S

then reconsider G = F | (Seg n) as FinSequence of S by FINSEQ_1:18;

reconsider F = F as FinSequence of S by A1;

for k, m being object st k <> m holds

G . k misses G . m

proof

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

assume A2: k <> m ; :: thesis: G . k misses G . m

end;assume A2: k <> m ; :: thesis: G . k misses G . m