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 f being Polynomial of n,L
for g being object
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 well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for g being object
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 well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f being Polynomial of n,L
for g being object
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 object
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 object ; :: 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 and
A2: p . (len p) = g by REWRITE1:def 3;
reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;
A3: 1 <= len p by NAT_1:14;
set h = p . l;
1 <= l + 1 by NAT_1:12;
then l + 1 in Seg (len p) by FINSEQ_1:1;
then A4: l + 1 in dom p by FINSEQ_1:def 3;

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, A2; :: 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 A5: 1 <= l by NAT_1:13;
l <= l + 1 by NAT_1:13;
then l in Seg (len p) by A5, FINSEQ_1:1;
then l in dom p by FINSEQ_1:def 3;
then [(p . l),g] in PolyRedRel (P,T) by A2, A4, REWRITE1:def 2;
then consider h9, g9 being object such that
A6: [(p . l),g] = [h9,g9] and
h9 in NonZero (Polynom-Ring (n,L)) and
A7: g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
g = g9 by A6, XTUPLE_0:1;
hence g is Polynomial of n,L by A7, POLYNOM1:def 11; :: thesis: verum

end;

end;