let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T
for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T
for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T
for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
let P be Subset of (Polynom-Ring n,L); :: thesis: for R being RedSequence of PolyRedRel P,T
for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
let R be RedSequence of PolyRedRel P,T; :: thesis: for i being Element of NAT st 1 <= i & i <= len R & len R > 1 holds
R . i is Polynomial of n,L
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len R & len R > 1 implies R . i is Polynomial of n,L )
assume A1: ( 1 <= i & i <= len R & 1 < len R ) ; :: thesis: R . i is Polynomial of n,L
then A2: i in dom R by FINSEQ_3:27;

now

per cases ( i <> len R or i = len R ) ;

case i <> len R ; :: thesis: R . i is Polynomial of n,L

then i < len R by A1, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= len R ) by NAT_1:11, NAT_1:13;
then i + 1 in dom R by FINSEQ_3:27;
then [(R . i),(R . (i + 1))] in PolyRedRel P,T by A2, REWRITE1:def 2;
then R . i in dom (PolyRedRel P,T) by RELAT_1:def 4;
then R . i in the carrier of (Polynom-Ring n,L) by XBOOLE_0:def 5;
hence R . i is Polynomial of n,L by POLYNOM1:def 27; :: thesis: verum

end;

case A3: i = len R ; :: thesis: R . i is Polynomial of n,L

A4: i - 1 is Element of NAT by A1, INT_1:18;
1 + (- 1) < i + (- 1) by A1, A3, XREAL_1:10;
then A5: 1 <= i - 1 by A4, NAT_1:14;
i - 1 <= len R by A3, XREAL_1:148;
then A6: i - 1 in dom R by A4, A5, FINSEQ_3:27;
i = (i - 1) + 1 ;
then [(R . (i - 1)),(R . i)] in PolyRedRel P,T by A2, A6, REWRITE1:def 2;
then R . i in rng (PolyRedRel P,T) by RELAT_1:def 5;
hence R . i is Polynomial of n,L by POLYNOM1:def 27; :: thesis: verum

end;

end;

end;

hence R . i is Polynomial of n,L ; :: thesis: verum