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 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 Def5;
A4: ( 0 -' 0 = 0 & len Fr = 1 ) by A1, XREAL_1:234;
0 in 1 by NAT_1:45;
then Fr . 0 = (seq1 . 0) * (seq2 . (0 -' 0)) by A2;
then Fr = <%((seq1 . 0) * (seq2 . 0))%> by A4, AFINSQ_1:38;
hence (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0) by A3, AFINSQ_2:65; :: thesis: verum