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 REAL by FINSEQ_1:102;
(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;