let x be real-valued FinSequence; :: thesis: for I being set st x is positive & I c= dom x & I <> {} holds
( Seq (x,I) is positive & Seq (x,I) <> {} )

let I be set ; :: thesis: ( x is positive & I c= dom x & I <> {} implies ( Seq (x,I) is positive & Seq (x,I) <> {} ) )
assume that
A2: x is positive and
A3: I c= dom x and
A4: I <> {} ; :: thesis: ( Seq (x,I) is positive & Seq (x,I) <> {} )
A5: dom x meets I by ;
for j being Nat st j in dom (Seq (x,I)) holds
0 < (Seq (x,I)) . j
proof
let j be Nat; :: thesis: ( j in dom (Seq (x,I)) implies 0 < (Seq (x,I)) . j )
assume A6: j in dom (Seq (x,I)) ; :: thesis: 0 < (Seq (x,I)) . j
reconsider sfi = Seq (x | I) as real-valued FinSequence ;
A9: (Sgm (dom (x | I))) . j in dom (x | I) by ;
A10: dom (x | I) c= dom x by RELAT_1:60;
(Seq (x,I)) . j = (x | I) . ((Sgm (dom (x | I))) . j) by
.= x . ((Sgm (dom (x | I))) . j) by ;
hence 0 < (Seq (x,I)) . j by A10, A2, A9; :: thesis: verum
end;
hence ( Seq (x,I) is positive & Seq (x,I) <> {} ) by ; :: thesis: verum