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
A4: len r1 = n and
A5: for i being Nat st 1 <= i & i <= n holds
r1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) and
A6: len r2 = n and
A7: 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 12;
let k be Nat; :: thesis: ( 1 <= k & k <= n implies r1 . k = r2 . k )
assume that
A8: 1 <= k and
A9: k <= n ; :: thesis: r1 . k = r2 . k
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
r1 . k0 = |(x0,(Base_FinSeq (n22,k0)))| * (Base_FinSeq (n22,k0)) by A5, A8, A9;
hence r1 . k = r2 . k by A7, A8, A9; :: thesis: verum

end;

hence r1 = r2 by A4, A6, FINSEQ_1:14; :: thesis: verum