let r1, r2 be FinSequence of REAL n; :: thesis: ( len r1 = n & ( for i being Nat st 1 <= i & i <= n holds
r1 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ) & len r2 = n & ( for i being Nat st 1 <= i & i <= n holds
r2 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ) implies r1 = r2 )
assume that
A6: len r1 = n and
A7: for i being Nat st 1 <= i & i <= n holds
r1 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) and
A8: len r2 = n and
A9: for i being Nat st 1 <= i & i <= n holds
r2 . i = |(x0,(Base_FinSeq n,i))| * (Base_FinSeq n,i) ; :: thesis: r1 = r2
for k being Nat st 1 <= k & k <= n holds
r1 . k = r2 . k

proof

reconsider n22 = n as Element of NAT by ORDINAL1:def 13;
let k be Nat; :: thesis: ( 1 <= k & k <= n implies r1 . k = r2 . k )
assume that
A10: 1 <= k and
A11: k <= n ; :: thesis: r1 . k = r2 . k
reconsider k0 = k as Element of NAT by ORDINAL1:def 13;
r1 . k0 = |(x0,(Base_FinSeq n22,k0))| * (Base_FinSeq n22,k0) by A7, A10, A11;
hence r1 . k = r2 . k by A9, A10, A11; :: thesis: verum

end;

hence r1 = r2 by A6, A8, FINSEQ_1:18; :: thesis: verum