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 Element of NAT st n in 0 + 1 holds
Fr . n = (seq1 . n) * (seq2 . (0 -' n)) and
A3: Sum Fr = (seq1 (##) seq2) . 0 by Def5;
0 in 1 by NAT_1:45;
then ( Fr . 0 = (seq1 . 0 ) * (seq2 . (0 -' 0 )) & 0 -' 0 = 0 & len Fr = 1 ) by A1, A2, XREAL_1:234;
then Fr = <%((seq1 . 0 ) * (seq2 . 0 ))%> by AFINSQ_1:38;
hence (seq1 (##) seq2) . 0 = (seq1 . 0 ) * (seq2 . 0 ) by A3, STIRL2_1:44; :: thesis: verum