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 f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g 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 f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g 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 f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g is Polynomial of n,L
let f be Polynomial of n,L; :: thesis: for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g is Polynomial of n,L
let g be set ; :: thesis: for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g is Polynomial of n,L
let P be Subset of (Polynom-Ring n,L); :: thesis: ( PolyRedRel P,T reduces f,g implies g is Polynomial of n,L )
set R = PolyRedRel P,T;
assume PolyRedRel P,T reduces f,g ; :: thesis: g is Polynomial of n,L
then consider p being RedSequence of PolyRedRel P,T such that
A1: ( p . 1 = f & p . (len p) = g ) by REWRITE1:def 3;
A3: 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 A4: l + 1 in dom p by FINSEQ_1:def 3;
set h = p . l;

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

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

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

end;

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

then 0 + 1 < l + 1 by A3, 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 A1, A4, REWRITE1:def 2;
then consider h', g' being set such that
A5: ( [(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 A5, MCART_1:def 2
.= g' by MCART_1:def 2 ;
hence g is Polynomial of n,L by A5, POLYNOM1:def 27; :: thesis: verum

end;

end;