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

( 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

hence
( x | i is positive & x | i <> {} )
by A3, A6; :: thesis: verum
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;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