let O be Ordinal; :: thesis: for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R st R is well-unital holds
( p `^ 0 = 1_ (O,R) & p `^ 1 = p )
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,R st R is well-unital holds
( p `^ 0 = 1_ (O,R) & p `^ 1 = p )
let p be Polynomial of O,R; :: thesis: ( R is well-unital implies ( p `^ 0 = 1_ (O,R) & p `^ 1 = p ) )
set PR = Polynom-Ring (O,R);
reconsider P = p as Element of (Polynom-Ring (O,R)) by POLYNOM1:def 11;
reconsider E = 1_ (O,R) as Element of (Polynom-Ring (O,R)) by POLYNOM1:def 11;
assume A1: R is well-unital ; :: thesis: ( p `^ 0 = 1_ (O,R) & p `^ 1 = p )
A2: for H being Element of (Polynom-Ring (O,R)) holds
( H * E = H & E * H = H )

proof

let H be Element of (Polynom-Ring (O,R)); :: thesis: ( H * E = H & E * H = H )
reconsider h = H as Polynomial of O,R by POLYNOM1:def 11;
( h *' (1_ (O,R)) = h & h = (1_ (O,R)) *' h ) by A1, POLYNOM1:29, POLYNOM1:30;
hence ( H * E = H & E * H = H ) by POLYNOM1:def 11; :: thesis: verum

end;

A3: Polynom-Ring (O,R) is unital

proof

take E ; :: according to GROUP_1:def 1 :: thesis: for b₁ being Element of the carrier of (Polynom-Ring (O,R)) holds
( b₁ * E = b₁ & E * b₁ = b₁ )
thus for b₁ being Element of the carrier of (Polynom-Ring (O,R)) holds
( b₁ * E = b₁ & E * b₁ = b₁ ) by A2; :: thesis: verum

end;

then 1_ (Polynom-Ring (O,R)) = E by A2, GROUP_1:def 4;
then (power (Polynom-Ring (O,R))) . (P,0) = E by GROUP_1:def 7;
hence ( p `^ 0 = 1_ (O,R) & p `^ 1 = p ) by A3, GROUP_1:50; :: thesis: verum