let F1, F2 be FinSequence; :: thesis: ( dom F1 = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom F1 holds
F1 . i = (i - 1) / (2 |^ n) ) & dom F2 = Seg ((2 |^ n) + 1) & ( for i being Nat st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ) implies F1 = F2 )
assume that
A2: dom F1 = Seg ((2 |^ n) + 1) and
A3: for i being Nat st i in dom F1 holds
F1 . i = (i - 1) / (2 |^ n) and
A4: dom F2 = Seg ((2 |^ n) + 1) and
A5: for i being Nat st i in dom F2 holds
F2 . i = (i - 1) / (2 |^ n) ; :: thesis: F1 = F2
consider X being set such that
A6: 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 A7: k in X ; :: thesis: F1 . k = F2 . k
hence F1 . k = (k - 1) / (2 |^ n) by A3, A6
.= F2 . k by A2, A4, A5, A6, A7 ;
:: thesis: verum

end;

hence F1 = F2 by A2, A4, A6, FINSEQ_1:13; :: thesis: verum