let Fr be XFinSequence of REAL ; :: thesis: ( ( dom Fr = 1 or len Fr = 1 ) implies Sum Fr = Fr . 0 )
assume ( dom Fr = 1 or len Fr = 1 ) ; :: thesis: Sum Fr = Fr . 0
then len Fr = 1 ;
then Fr = <%(Fr . 0)%> by AFINSQ_1:34;
hence Sum Fr = Fr . 0 by AFINSQ_2:53; :: thesis: verum