let Fr be XFinSequence of ; :: 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:38;
hence Sum Fr = Fr . 0 by AFINSQ_2:65; :: thesis: verum