A1: len f = len (Partial_Sums f) by Def13;

now :: thesis: ( ( len f > 0 & (Partial_Sums f) . (len f) is Element of Curves T ) or ( len f <= 0 & ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) ) )

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

case len f > 0 ; :: thesis: (Partial_Sums f) . (len f) is Element of Curves T

then 0 + 1 <= len f by NAT_1:13;
then len f in dom (Partial_Sums f) by A1, FINSEQ_3:25;
then (Partial_Sums f) . (len f) in rng (Partial_Sums f) by FUNCT_1:def 3;
hence (Partial_Sums f) . (len f) is Element of Curves T ; :: thesis: verum

end;

case A2: len f <= 0 ; :: thesis: ( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) )

{} is parametrized-curve PartFunc of R^1,T by Lm1, XBOOLE_1:2;
hence ( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) ) by A2, Th20; :: thesis: verum

end;

end;

end;

hence ( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) & ( not len f > 0 implies {} is Curve of T ) ) ; :: thesis: verum