let p be RedSequence of R; :: thesis: ( not p is trivial implies p is FinSequence-yielding )
assume not p is trivial ; :: thesis: p is FinSequence-yielding
then A1: 1 < len p by TOPREAL8:2;

now :: thesis: for x being object st x in dom p holds
p . x is FinSequence

let x be object ; :: thesis: ( x in dom p implies p . b₁ is FinSequence )
assume A2: x in dom p ; :: thesis: p . b₁ is FinSequence
then reconsider n = x as Nat ;
A3: ( 1 <= n & n <= len p ) by A2, FINSEQ_3:25;

per cases then ( n < len p or n = len p ) by XXREAL_0:1;

suppose n < len p ; :: thesis: p . b₁ is FinSequence

then A4: n + 1 <= len p by NAT_1:13;
1 + 0 <= n + 1 by A3, XREAL_1:8;
then n + 1 in dom p by A4, FINSEQ_3:25;
then [(p . n),(p . (n + 1))] in R by A2, REWRITE1:def 2;
then p . n in dom R by XTUPLE_0:def 12;
hence p . x is FinSequence ; :: thesis: verum

end;

suppose A5: n = len p ; :: thesis: p . b₁ is FinSequence

then reconsider n9 = n - 1 as Nat by CHORD:1;
1 < n9 + 1 by A1, A5;
then A6: 1 <= n9 by NAT_1:13;
n9 <= (len p) - 0 by A5, XREAL_1:10;
then n9 in dom p by A6, FINSEQ_3:25;
then [(p . n9),(p . (n9 + 1))] in R by A2, REWRITE1:def 2;
then p . n in rng R by XTUPLE_0:def 13;
hence p . x is FinSequence ; :: thesis: verum

end;

end;

end;

hence p is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum