let n be natural number ; :: thesis: Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*>
set N = Base_FinSeq ((n + 1),(n + 1));
set p = 0. (TOP-REAL n);
set q = <*1*>;
A1: dom (Base_FinSeq ((n + 1),(n + 1))) = Seg (n + 1) by FINSEQ_1:89
.= Seg (n + (len <*1*>)) by FINSEQ_1:39
.= Seg ((len (0. (TOP-REAL n))) + (len <*1*>)) by CARD_1:def 7 ;
A2: for k being natural number st k in dom (0. (TOP-REAL n)) holds
(Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k

proof

let k be natural number ; :: thesis: ( k in dom (0. (TOP-REAL n)) implies (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k )
assume k in dom (0. (TOP-REAL n)) ; :: thesis: (Base_FinSeq ((n + 1),(n + 1))) . k = (0. (TOP-REAL n)) . k
then A3: k in Seg n by FINSEQ_1:89;
then A4: ( 1 <= k & k <= n ) by FINSEQ_1:1;
0 + n <= 1 + n by XREAL_1:6;
then A5: k <= n + 1 by A4, XXREAL_0:2;
A6: n + 1 <> k by A4, NAT_1:13;
thus (Base_FinSeq ((n + 1),(n + 1))) . k = 0 by A5, A4, A6, MATRIXR2:76
.= (0* n) . k by A3, FINSEQ_2:57
.= (0. (TOP-REAL n)) . k by EUCLID:70 ; :: thesis: verum

end;

for k being natural number st k in dom <*1*> holds
(Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k

proof

let k be natural number ; :: thesis: ( k in dom <*1*> implies (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k )
assume k in dom <*1*> ; :: thesis: (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k
then k in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A7: k = 1 by TARSKI:def 1;
A8: 0 + 1 <= n + 1 by XREAL_1:6;
thus (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = (Base_FinSeq ((n + 1),(n + 1))) . (n + 1) by A7, CARD_1:def 7
.= 1 by A8, MATRIXR2:75
.= <*1*> . k by A7, FINSEQ_1:40 ; :: thesis: verum

end;

hence Base_FinSeq ((n + 1),(n + 1)) = (0. (TOP-REAL n)) ^ <*1*> by A1, A2, FINSEQ_1:def 7; :: thesis: verum