let n be Nat; :: 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 Nat 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 Nat; :: 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 k in Seg n by FINSEQ_1:89;
then A3: ( 1 <= k & k <= n ) by FINSEQ_1:1;
0 + n <= 1 + n by XREAL_1:6;
then A4: k <= n + 1 by A3, XXREAL_0:2;
A5: n + 1 <> k by A3, NAT_1:13;
thus (Base_FinSeq ((n + 1),(n + 1))) . k = 0 by A4, A3, A5, MATRIXR2:76
.= (0* n) . k
.= (0. (TOP-REAL n)) . k by EUCLID:70 ; :: thesis: verum
end;
for k being Nat st k in dom <*1*> holds
(Base_FinSeq ((n + 1),(n + 1))) . ((len (0. (TOP-REAL n))) + k) = <*1*> . k
proof
let k be Nat; :: 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 A6: k = 1 by TARSKI:def 1;
A7: 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 A6, CARD_1:def 7
.= 1 by A7, MATRIXR2:75
.= <*1*> . k by A6, 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