let t, u be FinSequence of S; :: thesis: ( dom t = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & t . m = S -head ((S ^^ k) -tail p) ) ) & dom u = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & u . m = S -head ((S ^^ k) -tail p) ) ) implies t = u )
assume that
A1: dom t = Seg n and
A2: for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & t . m = S -head ((S ^^ k) -tail p) ) and
A3: dom u = Seg n and
A4: for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & u . m = S -head ((S ^^ k) -tail p) ) ; :: thesis: t = u
for i being Nat st i in dom t holds
t . i = u . i

proof

let i be Nat; :: thesis: ( i in dom t implies t . i = u . i )
assume A5: i in dom t ; :: thesis: t . i = u . i
then consider k being Nat such that
A7: i = k + 1 and
A8: t . i = S -head ((S ^^ k) -tail p) by A1, A2;
consider l being Nat such that
A9: i = l + 1 and
A10: u . i = S -head ((S ^^ l) -tail p) by A1, A4, A5;
thus t . i = u . i by A7, A8, A9, A10; :: thesis: verum

end;

hence t = u by A1, A3, FINSEQ_1:13; :: thesis: verum