let n be Nat; :: thesis: Base_FinSeq ((n + 1),(n + 1)) = (0. ()) ^ <*1*>
set N = Base_FinSeq ((n + 1),(n + 1));
set p = 0. ();
set q = <*1*>;
A1: dom (Base_FinSeq ((n + 1),(n + 1))) = Seg (n + 1) by FINSEQ_1:89
.= Seg (n + ()) by FINSEQ_1:39
.= Seg ((len (0. ())) + ()) by CARD_1:def 7 ;
A2: for k being Nat st k in dom (0. ()) holds
(Base_FinSeq ((n + 1),(n + 1))) . k = (0. ()) . k
proof
let k be Nat; :: thesis: ( k in dom (0. ()) implies (Base_FinSeq ((n + 1),(n + 1))) . k = (0. ()) . k )
assume k in dom (0. ()) ; :: thesis: (Base_FinSeq ((n + 1),(n + 1))) . k = (0. ()) . 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 ;
A5: n + 1 <> k by ;
thus (Base_FinSeq ((n + 1),(n + 1))) . k = 0 by
.= (0* n) . k
.= (0. ()) . 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. ())) + k) = <*1*> . k
proof
let k be Nat; :: thesis: ( k in dom <*1*> implies (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. ())) + k) = <*1*> . k )
assume k in dom <*1*> ; :: thesis: (Base_FinSeq ((n + 1),(n + 1))) . ((len (0. ())) + k) = <*1*> . k
then k in {1} by ;
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. ())) + k) = (Base_FinSeq ((n + 1),(n + 1))) . (n + 1) by
.= 1 by
.= <*1*> . k by ; :: thesis: verum
end;
hence Base_FinSeq ((n + 1),(n + 1)) = (0. ()) ^ <*1*> by ; :: thesis: verum