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
reconsider G = F | (Seg n) as FinSequence of S by A1, FINSEQ_1:23;
reconsider F = F as FinSequence of S by A1;
A2: for k, m being set st k <> m holds
G . k misses G . m

proof

let k, m be set ; :: thesis: ( k <> m implies G . k misses G . m )
assume A3: k <> m ; :: thesis: G . k misses G . m

per cases ( ( k in dom G & m in dom G ) or not k in dom G or not m in dom G ) ;

suppose A4: ( k in dom G & m in dom G ) ; :: thesis: G . k misses G . m

A5: ( G . k = F . k & G . m = F . m ) by A4, FUNCT_1:70;
thus G . k misses G . m by A1, A3, A5, PROB_2:def 3; :: thesis: verum

end;

suppose A6: ( not k in dom G or not m in dom G ) ; :: thesis: G . k misses G . m

A7: ( G . k = {} or G . m = {} ) by A6, FUNCT_1:def 4;
thus G . k misses G . m by A7, XBOOLE_1:65; :: thesis: verum

end;

end;

end;

thus F | (Seg n) is Finite_Sep_Sequence of S by A2, PROB_2:def 3; :: thesis: verum