let T be non empty 1-sorted ; :: thesis: for F, G being SetSequence of the carrier of T
for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F
let F, G be SetSequence of the carrier of T; :: thesis: for A being Subset of T st G is subsequence of F & ( for i being Nat holds F . i = A ) holds
G = F
let A be Subset of T; :: thesis: ( G is subsequence of F & ( for i being Nat holds F . i = A ) implies G = F )
assume that
A1: G is subsequence of F and
A2: for i being Nat holds F . i = A ; :: thesis: G = F
consider NS being increasing sequence of NAT such that
A3: G = F * NS by A1, VALUED_0:def 17;
A4: for i being Element of NAT holds G . i = F . i

proof

let i be Element of NAT ; :: thesis: G . i = F . i
dom NS = NAT by FUNCT_2:def 1;
then G . i = F . (NS . i) by A3, FUNCT_1:23
.= A by A2
.= F . i by A2 ;
hence G . i = F . i ; :: thesis: verum

end;

A5: ( NAT = dom G & NAT = dom F ) by FUNCT_2:def 1;
for x being set st x in dom F holds
F . x = G . x by A4;
hence G = F by A5, FUNCT_1:9; :: thesis: verum