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 A4, A3, XBOOLE_1:28;
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 A6, FUNCT_1:11;
A10: dom (x | I) c= dom x by RELAT_1:60;
(Seq (x,I)) . j = (x | I) . ((Sgm (dom (x | I))) . j) by A6, FUNCT_1:12
.= x . ((Sgm (dom (x | I))) . j) by A9, FUNCT_1:47 ;
hence 0 < (Seq (x,I)) . j by A10, A2, A9; :: thesis: verum

end;

hence ( Seq (x,I) is positive & Seq (x,I) <> {} ) by A5, RELAT_1:66, FINSEQ_1:97; :: thesis: verum