len (f | j) = min (j,(len f)) by FINSEQ_2:21;
then A0: j >= len (f | j) by XXREAL_0:17;
per cases ( j in dom f or not j in dom f ) ;
suppose Q0: j in dom f ; :: thesis: not (f | j) . i is negative
per cases ( i in dom (f | j) or not i in dom (f | j) ) ;
suppose i in dom (f | j) ; :: thesis: not (f | j) . i is negative
then ( len (f | j) >= i & i >= 1 ) by FINSEQ_3:25;
then A2: ( 1 <= i & i <= j ) by A0, XXREAL_0:2;
reconsider f = f as FinSequence of COMPLEX by RVSUM_1:146;
(f | j) . i = f . i by Q0, A2, NEWTON02:107;
hence not (f | j) . i is negative ; :: thesis: verum
end;
suppose not i in dom (f | j) ; :: thesis: not (f | j) . i is negative
hence not (f | j) . i is negative by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
suppose not j in dom f ; :: thesis: not (f | j) . i is negative
then ( j > len f or j < 1 ) by FINSEQ_3:25;
then ( f | j = f or j = 0 ) by FINSEQ_1:58, NAT_1:14;
hence not (f | j) . i is negative ; :: thesis: verum
end;
end;