let R be domRing; :: thesis: for n being non empty Ordinal
for a being Element of R
for i being Element of n holds degree ((1_1 (i,R)) + (a | (n,R))) = 1
let n be non empty Ordinal; :: thesis: for a being Element of R
for i being Element of n holds degree ((1_1 (i,R)) + (a | (n,R))) = 1
let a be Element of R; :: thesis: for i being Element of n holds degree ((1_1 (i,R)) + (a | (n,R))) = 1
let i be Element of n; :: thesis: degree ((1_1 (i,R)) + (a | (n,R))) = 1
set p = 1_1 (i,R);
set q = a | (n,R);
set UBi = UnitBag i;
reconsider p0 = (1_1 (i,R)) + (a | (n,R)) as Polynomial of n,R ;
A1: Support p0 c= {(UnitBag i)} \/ {(EmptyBag n)} by Th9;
dom p0 = Bags n by FUNCT_2:def 1;
then A2: UnitBag i in dom p0 by PRE_POLY:def 12;
( (1_1 (i,R)) . (UnitBag i) = 1. R & (a | (n,R)) . (UnitBag i) = 0. R ) by Th6;
then p0 . (UnitBag i) = (1. R) + (0. R) by POLYNOM1:15
.= 1. R ;
then p0 . (UnitBag i) <> 0. R ;
then A4: UnitBag i in Support p0 by A2, POLYNOM1:def 3;
then Support p0 <> {} by XBOOLE_0:def 1;
then A5: p0 <> 0_ (n,R) by Th1;
A6: for o being object holds
( not o in Support p0 or o = UnitBag i or o = EmptyBag n )

proof

let o be object ; :: thesis: ( not o in Support p0 or o = UnitBag i or o = EmptyBag n )
assume o in Support p0 ; :: thesis: ( o = UnitBag i or o = EmptyBag n )
then ( o in {(UnitBag i)} or o in {(EmptyBag n)} ) by A1, XBOOLE_0:def 3;
hence ( o = UnitBag i or o = EmptyBag n ) by TARSKI:def 1; :: thesis: verum

end;

A8: for s1 being bag of n st s1 in Support p0 holds
degree s1 <= degree (UnitBag i)

proof

let s1 be bag of n; :: thesis: ( s1 in Support p0 implies degree s1 <= degree (UnitBag i) )
assume s1 in Support p0 ; :: thesis: degree s1 <= degree (UnitBag i)

per cases then ( s1 = UnitBag i or s1 = EmptyBag n ) by A6;

suppose s1 = UnitBag i ; :: thesis: degree s1 <= degree (UnitBag i)

hence degree s1 <= degree (UnitBag i) ; :: thesis: verum

end;

suppose s1 = EmptyBag n ; :: thesis: degree s1 <= degree (UnitBag i)

hence degree s1 <= degree (UnitBag i) by Th10; :: thesis: verum

end;

end;

end;

consider s being bag of n such that
A12: s = UnitBag i ;
degree p0 = degree s by A8, A5, A12, A4, HILB10_5:def 3;
hence degree ((1_1 (i,R)) + (a | (n,R))) = 1 by A12, Th11; :: thesis: verum