A1: len f = len (accum f) by Def11;

now

per cases ( len f > 0 or len f <= 0 ) ;

case len f > 0 ; :: thesis: (accum f) . (len f) is Element of REAL n

then 0 + 1 <= len f by NAT_1:13;
then len f in dom (accum f) by A1, FINSEQ_3:27;
then (accum f) . (len f) in rng (accum f) by FUNCT_1:def 5;
hence (accum f) . (len f) is Element of REAL n ; :: thesis: verum

end;

case len f <= 0 ; :: thesis: ( ( len f > 0 implies (accum f) . (len f) is Element of REAL n ) & ( not len f > 0 implies 0* n is Element of REAL n ) )

hence ( ( len f > 0 implies (accum f) . (len f) is Element of REAL n ) & ( not len f > 0 implies 0* n is Element of REAL n ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( len f > 0 implies (accum f) . (len f) is Element of REAL n ) & ( not len f > 0 implies 0* n is Element of REAL n ) ) ; :: thesis: verum