set g = f | (Seg n);
for k being Nat st k in dom (f | (Seg n)) holds
(f | (Seg n)) . k > 0
proof
let k be Nat; :: 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 A3: 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, A3; :: thesis: verum
end;
hence f | (Seg n) is positive ; :: thesis: verum