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

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

hence
F1 = F2
by A2, A4, A6, FINSEQ_1:13; :: thesis: verum
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;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