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 & p . (len p) = g ) by REWRITE1:def 3;
A4: 1 <= len p by NAT_1:14;
reconsider l = (len p) - 1 as Element of NAT by INT_1:18, NAT_1:14;
( 1 <= l + 1 & l + 1 <= len p ) by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:3;
then A5: l + 1 in dom p by FINSEQ_1:def 3;
set q = p . (1 + 1);
set h = p . l;

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

end;

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

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

end;

end;

end;

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

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; :: 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 ( 1 <= l & l <= l + 1 ) by NAT_1:13;
then l in Seg (len p) by FINSEQ_1:3;
then l in dom p by FINSEQ_1:def 3;
then [(p . l),g] in PolyRedRel P,T by A2, A5, REWRITE1:def 2;
then consider h', g' being set such that
A9: ( [(p . l),g] = [h',g'] & h' in NonZero (Polynom-Ring n,L) & g' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
g = [h',g'] `2 by A9, MCART_1:def 2
.= g' by MCART_1:def 2 ;
hence g is Polynomial of n,L by A9, POLYNOM1:def 27; :: thesis: verum

end;

end;

end;

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