let x be real-valued FinSequence; :: thesis: for i being Nat st x is positive & 1 <= i & i <= len x holds
( x | i is positive & x | i <> {} )
let i be Nat; :: thesis: ( x is positive & 1 <= i & i <= len x implies ( x | i is positive & x | i <> {} ) )
assume that
A2: x is positive and
A3: 1 <= i and
A4: i <= len x ; :: thesis: ( x | i is positive & x | i <> {} )
A5: dom (x | i) c= dom x by RELAT_1:60;
A6: len (x | i) = i by A4, FINSEQ_1:59;
for j being Nat st j in dom (x | i) holds
0 < (x | i) . j
proof
let j be Nat; :: thesis: ( j in dom (x | i) implies 0 < (x | i) . j )
assume A7: j in dom (x | i) ; :: thesis: 0 < (x | i) . j
then A8: 0 < x . j by A2, A5;
Seg i c= Seg (len x) by A4, FINSEQ_1:5;
then Seg i c= dom x by FINSEQ_1:def 3;
then dom (x | i) = Seg i by RELAT_1:62;
then j <= i by A7, FINSEQ_1:1;
hence 0 < (x | i) . j by A8, FINSEQ_3:112; :: thesis: verum
end;
hence ( x | i is positive & x | i <> {} ) by A3, A6; :: thesis: verum