let x be real-valued FinSequence; 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 ; ( 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 <> {}
; ( 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;
( j in dom (Seq (x,I)) implies 0 < (Seq (x,I)) . j )
assume A6:
j in dom (Seq (x,I))
;
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;
verum
end;
hence
( Seq (x,I) is positive & Seq (x,I) <> {} )
by A5, RELAT_1:66, FINSEQ_1:97; verum