let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f, 0_ n,L holds
f has_a_Standard_Representation_of P,T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f, 0_ n,L holds
f has_a_Standard_Representation_of P,T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f, 0_ n,L holds
f has_a_Standard_Representation_of P,T
let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f, 0_ n,L holds
f has_a_Standard_Representation_of P,T
let P be non empty Subset of (Polynom-Ring n,L); :: thesis: ( PolyRedRel P,T reduces f, 0_ n,L implies f has_a_Standard_Representation_of P,T )
assume A1: PolyRedRel P,T reduces f, 0_ n,L ; :: thesis: f has_a_Standard_Representation_of P,T
reconsider f' = f as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
then consider A being LeftLinearCombination of P such that
A2: ( f' = (0. (Polynom-Ring n,L)) + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) ) by A1, Lm5;
A3: f = Sum A by A2, RLVECT_1:def 7;

now

let i be Element of NAT ; :: thesis: ( i in dom A implies ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT (m *' p),T <= HT f,T,T ) )
assume A4: i in dom A ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT (m *' p),T <= HT f,T,T )
then consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A5: ( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) by A2;
thus ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT (m *' p),T <= HT f,T,T ) by A4, A5, PARTFUN1:def 8; :: thesis: verum

end;

then A is_Standard_Representation_of f,P, HT f,T,T by A3, Def7;
then A is_Standard_Representation_of f,P,T by Def8;
hence f has_a_Standard_Representation_of P,T by Def10; :: thesis: verum