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;
for i being Nat holds G . i = F . i
proof
let i be Nat; :: thesis: G . i = F . i
reconsider i = i as Element of NAT by ORDINAL1:def 12;
dom NS = NAT by FUNCT_2:def 1;
then G . i = F . (NS . i) by A3, FUNCT_1:13
.= A by A2
.= F . i by A2 ;
hence G . i = F . i ; :: thesis: verum
end;
then A4: for x being object st x in dom F holds
F . x = G . x ;
( NAT = dom G & NAT = dom F ) by FUNCT_2:def 1;
hence G = F by A4, FUNCT_1:2; :: thesis: verum