let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
(Up p,T,i) + (Low p,T,i) = p
let T be connected TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
(Up p,T,i) + (Low p,T,i) = p
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
(Up p,T,i) + (Low p,T,i) = p
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
(Up p,T,i) + (Low p,T,i) = p
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies (Up p,T,i) + (Low p,T,i) = p )
assume A1: i <= card (Support p) ; :: thesis: (Up p,T,i) + (Low p,T,i) = p
set u = (Up p,T,i) + (Low p,T,i);

A2: now

let x be set ; :: thesis: ( x in Support ((Up p,T,i) + (Low p,T,i)) implies x in Support p )
assume A3: x in Support ((Up p,T,i) + (Low p,T,i)) ; :: thesis: x in Support p
A4: Support ((Up p,T,i) + (Low p,T,i)) c= (Support (Up p,T,i)) \/ (Support (Low p,T,i)) by POLYNOM1:79;
( Support (Up p,T,i) c= Support p & Support (Low p,T,i) c= Support p ) by A1, Th26;
then (Support (Up p,T,i)) \/ (Support (Low p,T,i)) c= Support p by XBOOLE_1:8;
then Support ((Up p,T,i) + (Low p,T,i)) c= Support p by A4, XBOOLE_1:1;
hence x in Support p by A3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in Support p implies x in Support ((Up p,T,i) + (Low p,T,i)) )
assume A5: x in Support p ; :: thesis: x in Support ((Up p,T,i) + (Low p,T,i))
then reconsider x' = x as Element of Bags n ;
A6: ((Up p,T,i) + (Low p,T,i)) . x' = ((Up p,T,i) . x') + ((Low p,T,i) . x') by POLYNOM1:def 21;
A7: p . x' <> 0. L by A5, POLYNOM1:def 9;

now

per cases ( x' in Support (Up p,T,i) or x' in Support (Low p,T,i) ) by A1, A5, Th28;

case A8: x' in Support (Up p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x' = p . x'

hence ((Up p,T,i) + (Low p,T,i)) . x' = ((Up p,T,i) . x') + (0. L) by A1, A6, Th32
.= (Up p,T,i) . x' by RLVECT_1:def 7
.= p . x' by A1, A8, Th32 ;
:: thesis: verum

end;

case A9: x' in Support (Low p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x' = p . x'

hence ((Up p,T,i) + (Low p,T,i)) . x' = (0. L) + ((Low p,T,i) . x') by A1, A6, Th31
.= (Low p,T,i) . x' by ALGSTR_1:def 5
.= p . x' by A1, A9, Th31 ;
:: thesis: verum

end;

end;

end;

hence x in Support ((Up p,T,i) + (Low p,T,i)) by A7, POLYNOM1:def 9; :: thesis: verum

end;

then A10: Support ((Up p,T,i) + (Low p,T,i)) = Support p by A2, TARSKI:2;
A11: dom p = Bags n by FUNCT_2:def 1
.= dom ((Up p,T,i) + (Low p,T,i)) by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom p implies p . x = ((Up p,T,i) + (Low p,T,i)) . x )
assume x in dom p ; :: thesis: p . x = ((Up p,T,i) + (Low p,T,i)) . x
then reconsider x' = x as Element of Bags n ;
A12: ((Up p,T,i) + (Low p,T,i)) . x' = ((Up p,T,i) . x') + ((Low p,T,i) . x') by POLYNOM1:def 21;

now

per cases ( x' in Support p or not x' in Support p ) ;

case A13: x' in Support p ; :: thesis: p . x' = ((Up p,T,i) + (Low p,T,i)) . x'

now

per cases ( x' in Support (Up p,T,i) or x' in Support (Low p,T,i) ) by A1, A13, Th28;

case A14: x' in Support (Up p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x' = p . x'

hence ((Up p,T,i) + (Low p,T,i)) . x' = ((Up p,T,i) . x') + (0. L) by A1, A12, Th32
.= (Up p,T,i) . x' by RLVECT_1:def 7
.= p . x' by A1, A14, Th32 ;
:: thesis: verum

end;

case A15: x' in Support (Low p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x' = p . x'

hence ((Up p,T,i) + (Low p,T,i)) . x' = (0. L) + ((Low p,T,i) . x') by A1, A12, Th31
.= (Low p,T,i) . x' by ALGSTR_1:def 5
.= p . x' by A1, A15, Th31 ;
:: thesis: verum

end;

end;

end;

hence p . x' = ((Up p,T,i) + (Low p,T,i)) . x' ; :: thesis: verum

end;

case A16: not x' in Support p ; :: thesis: p . x' = ((Up p,T,i) + (Low p,T,i)) . x'

hence p . x' = 0. L by POLYNOM1:def 9
.= ((Up p,T,i) + (Low p,T,i)) . x' by A10, A16, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

hence p . x = ((Up p,T,i) + (Low p,T,i)) . x ; :: thesis: verum

end;

hence (Up p,T,i) + (Low p,T,i) = p by A11, FUNCT_1:9; :: thesis: verum