set g = f | (Seg n);
let k be Nat; :: according to RVSUM_3:def 1 :: thesis: ( k in dom (f | (Seg n)) implies (f | (Seg n)) . k > 0 )
A1: dom (f | (Seg n)) c= dom f by RELAT_1:60;
assume A2: k in dom (f | (Seg n)) ; :: thesis: (f | (Seg n)) . k > 0
then f . k > 0 by PosDef, A1;
hence (f | (Seg n)) . k > 0 by FUNCT_1:47, A2; :: thesis: verum