let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 that

A1: 1 <= i and

A2: i <= len R and

A3: 1 < len R ; :: thesis: R . i is Polynomial of n,L

A4: i in dom R by A1, A2, FINSEQ_3:25;

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 that

A1: 1 <= i and

A2: i <= len R and

A3: 1 < len R ; :: thesis: R . i is Polynomial of n,L

A4: i in dom R by A1, A2, FINSEQ_3:25;

now :: thesis: ( ( i <> len R & R . i is Polynomial of n,L ) or ( i = len R & R . i is Polynomial of n,L ) )end;

hence
R . i is Polynomial of n,L
; :: thesis: verumper cases
( i <> len R or i = len R )
;

end;

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

then
i < len R
by A2, 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:25;

then [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by A4, REWRITE1:def 2;

then R . i in dom (PolyRedRel (P,T)) by XTUPLE_0:def 12;

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 11; :: thesis: verum

end;then ( 1 <= i + 1 & i + 1 <= len R ) by NAT_1:11, NAT_1:13;

then i + 1 in dom R by FINSEQ_3:25;

then [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by A4, REWRITE1:def 2;

then R . i in dom (PolyRedRel (P,T)) by XTUPLE_0:def 12;

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 11; :: thesis: verum

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

A6:
i - 1 is Element of NAT
by A1, INT_1:5;

1 + (- 1) < i + (- 1) by A3, A5, XREAL_1:8;

then A7: 1 <= i - 1 by A6, NAT_1:14;

A8: i = (i - 1) + 1 ;

i - 1 <= len R by A5, XREAL_1:146;

then i - 1 in dom R by A6, A7, FINSEQ_3:25;

then [(R . (i - 1)),(R . i)] in PolyRedRel (P,T) by A4, A8, REWRITE1:def 2;

then R . i in rng (PolyRedRel (P,T)) by XTUPLE_0:def 13;

hence R . i is Polynomial of n,L by POLYNOM1:def 11; :: thesis: verum

end;1 + (- 1) < i + (- 1) by A3, A5, XREAL_1:8;

then A7: 1 <= i - 1 by A6, NAT_1:14;

A8: i = (i - 1) + 1 ;

i - 1 <= len R by A5, XREAL_1:146;

then i - 1 in dom R by A6, A7, FINSEQ_3:25;

then [(R . (i - 1)),(R . i)] in PolyRedRel (P,T) by A4, A8, REWRITE1:def 2;

then R . i in rng (PolyRedRel (P,T)) by XTUPLE_0:def 13;

hence R . i is Polynomial of n,L by POLYNOM1:def 11; :: thesis: verum