let seq1, seq2 be Real_Sequence; :: thesis: (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0)
set S = (seq1 . 0) * (seq2 . 0);
consider Fr being XFinSequence of REAL such that
A1: dom Fr = 0 + 1 and
A2: for n being Nat st n in 0 + 1 holds
Fr . n = (seq1 . n) * (seq2 . (0 -' n)) and
A3: Sum Fr = (seq1 (##) seq2) . 0 by Def4;
A4: ( 0 -' 0 = 0 & len Fr = 1 ) by A1, XREAL_1:232;
0 in Segm 1 by NAT_1:44;
then Fr . 0 = (seq1 . 0) * (seq2 . (0 -' 0)) by A2;
then Fr = <%((seq1 . 0) * (seq2 . 0))%> by A4, AFINSQ_1:34;
hence (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0) by A3, AFINSQ_2:53; :: thesis: verum