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 a, b being set st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b 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 a, b being set st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b 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 a, b being set st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for a, b being set st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
let f, g be set ; :: thesis: ( f <> g & PolyRedRel (P,T) reduces f,g implies ( f is Polynomial of n,L & g is Polynomial of n,L ) )
set R = PolyRedRel (P,T);
assume A1: f <> g ; :: thesis: ( not PolyRedRel (P,T) reduces f,g or ( f is Polynomial of n,L & g is Polynomial of n,L ) )
assume PolyRedRel (P,T) reduces f,g ; :: thesis: ( f is Polynomial of n,L & g is Polynomial of n,L )
then consider p being RedSequence of PolyRedRel (P,T) such that
A2: p . 1 = f and
A3: p . (len p) = g by REWRITE1:def 3;
reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;
set q = p . (1 + 1);
set h = p . l;
A4: 1 <= len p by NAT_1:14;

now

per cases ( len p = 1 or len p <> 1 ) ;

case len p = 1 ; :: thesis: f is Polynomial of n,L

hence f is Polynomial of n,L by A1, A2, A3; :: thesis: verum

end;

case len p <> 1 ; :: thesis: f is Polynomial of n,L

then 1 < len p by A4, XXREAL_0:1;
then 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg (len p) by FINSEQ_1:1;
then A5: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg (len p) by A4, FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then [f,(p . (1 + 1))] in PolyRedRel (P,T) by A2, A5, REWRITE1:def 2;
then consider h9, g9 being set such that
A6: [f,(p . (1 + 1))] = [h9,g9] and
A7: h9 in NonZero (Polynom-Ring (n,L)) and
g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
f = [h9,g9] `1 by A6, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
hence f is Polynomial of n,L by A7, POLYNOM1:def 10; :: thesis: verum

end;

end;

end;

hence f is Polynomial of n,L ; :: thesis: g is Polynomial of n,L
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:1;
then A8: l + 1 in dom p by FINSEQ_1:def 3;

now

per cases ( len p = 1 or len p <> 1 ) ;

case len p = 1 ; :: thesis: g is Polynomial of n,L

hence g is Polynomial of n,L by A1, A2, A3; :: thesis: verum

end;

case len p <> 1 ; :: thesis: g is Polynomial of n,L

then 0 + 1 < l + 1 by A4, XXREAL_0:1;
then A9: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg (len p) by A9, FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then [(p . l),g] in PolyRedRel (P,T) by A3, A8, REWRITE1:def 2;
then consider h9, g9 being set such that
A10: [(p . l),g] = [h9,g9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A11: g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
g = [h9,g9] `2 by A10, MCART_1:def 2
.= g9 by MCART_1:def 2 ;
hence g is Polynomial of n,L by A11, POLYNOM1:def 10; :: thesis: verum

end;

end;

end;

hence g is Polynomial of n,L ; :: thesis: verum