let F1, F2 be FinSequence; :: thesis: ( dom F1 = Seg (n + 1) & ( for i being Nat st i in dom F1 holds
F1 . i = ((i - 1) * ((n + 1) - i)) + 1 ) & dom F2 = Seg (n + 1) & ( for i being Nat st i in dom F2 holds
F2 . i = ((i - 1) * ((n + 1) - i)) + 1 ) implies F1 = F2 )
assume A1: ( dom F1 = Seg (n + 1) & ( for i being Nat st i in dom F1 holds
F1 . i = ((i - 1) * ((n + 1) - i)) + 1 ) & dom F2 = Seg (n + 1) & ( for i being Nat st i in dom F2 holds
F2 . i = ((i - 1) * ((n + 1) - i)) + 1 ) ) ; :: thesis: F1 = F2
consider X being set such that
A2: 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 B1: k in X ; :: thesis: F1 . k = F2 . k
F1 . k = ((k - 1) * ((n + 1) - k)) + 1 by A1, A2, B1
.= F2 . k by A1, A2, B1 ;
hence F1 . k = F2 . k ; :: thesis: verum

end;

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