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

( 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

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