let F1, F2 be FinSequence; :: thesis: ( dom F1 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F1 holds
F1 . i = (i - 1) / (2 |^ n) ) & dom F2 = Seg ((2 |^ n) + 1) & ( for i being Element of NAT st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ) implies F1 = F2 )
assume that
A1: dom F1 = Seg ((2 |^ n) + 1) and
A2: for i being Element of NAT st i in dom F1 holds
F1 . i = (i - 1) / (2 |^ n) and
A3: dom F2 = Seg ((2 |^ n) + 1) and
A4: for i being Element of NAT st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ; :: thesis: F1 = F2
consider X being set such that
A5: X = dom F1 ;
for k being Nat st k in X holds
F1 . k = F2 . k

proof

let k be Nat; :: thesis: ( k in X implies F1 . k = F2 . k )
assume A6: k in X ; :: thesis: F1 . k = F2 . k
hence F1 . k = (k - 1) / (2 |^ n) by A2, A5
.= F2 . k by A1, A3, A4, A5, A6 ;
:: thesis: verum

end;

hence F1 = F2 by A1, A3, A5, FINSEQ_1:17; :: thesis: verum