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 )
set u = (Up p,T,i) + (Low p,T,i);
assume A1: i <= card (Support p) ; :: thesis: (Up p,T,i) + (Low p,T,i) = p

A2: now

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

A5: now

per cases ( x9 in Support (Up p,T,i) or x9 in Support (Low p,T,i) ) by A1, A3, Th28;

case A6: x9 in Support (Up p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x9 = p . x9

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

end;

case A7: x9 in Support (Low p,T,i) ; :: thesis: ((Up p,T,i) + (Low p,T,i)) . x9 = p . x9

hence ((Up p,T,i) + (Low p,T,i)) . x9 = (0. L) + ((Low p,T,i) . x9) by A1, A4, Th31
.= (Low p,T,i) . x9 by ALGSTR_1:def 5
.= p . x9 by A1, A7, Th31 ;
:: thesis: verum

end;

end;

end;

p . x9 <> 0. L by A3, POLYNOM1:def 9;
hence x in Support ((Up p,T,i) + (Low p,T,i)) by A5, POLYNOM1:def 9; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in Support ((Up p,T,i) + (Low p,T,i)) implies x in Support p )
( 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) + (Low p,T,i)) c= (Support (Up p,T,i)) \/ (Support (Low p,T,i)) & (Support (Up p,T,i)) \/ (Support (Low p,T,i)) c= Support p ) by POLYNOM1:79, XBOOLE_1:8;
then A8: Support ((Up p,T,i) + (Low p,T,i)) c= Support p by XBOOLE_1:1;
assume x in Support ((Up p,T,i) + (Low p,T,i)) ; :: thesis: x in Support p
hence x in Support p by A8; :: thesis: verum

end;

then A9: Support ((Up p,T,i) + (Low p,T,i)) = Support p by A2, TARSKI:2;

A10: 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 x9 = x as Element of Bags n ;
A11: ((Up p,T,i) + (Low p,T,i)) . x9 = ((Up p,T,i) . x9) + ((Low p,T,i) . x9) by POLYNOM1:def 21;

now

per cases ( x9 in Support p or not x9 in Support p ) ;

case A12: x9 in Support p ; :: thesis: p . x9 = ((Up p,T,i) + (Low p,T,i)) . x9

now

per cases ( x9 in Support (Up p,T,i) or x9 in Support (Low p,T,i) ) by A1, A12, Th28;

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

hence ((Up p,T,i) + (Low p,T,i)) . x9 = ((Up p,T,i) . x9) + (0. L) by A1, A11, Th32
.= (Up p,T,i) . x9 by RLVECT_1:def 7
.= p . x9 by A1, A13, Th32 ;
:: thesis: verum

end;

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

hence ((Up p,T,i) + (Low p,T,i)) . x9 = (0. L) + ((Low p,T,i) . x9) by A1, A11, Th31
.= (Low p,T,i) . x9 by ALGSTR_1:def 5
.= p . x9 by A1, A14, Th31 ;
:: thesis: verum

end;

end;

end;

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

end;

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

hence p . x9 = 0. L by POLYNOM1:def 9
.= ((Up p,T,i) + (Low p,T,i)) . x9 by A9, A15, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

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

end;

dom p = Bags n by FUNCT_2:def 1
.= dom ((Up p,T,i) + (Low p,T,i)) by FUNCT_2:def 1 ;
hence (Up p,T,i) + (Low p,T,i) = p by A10, FUNCT_1:9; :: thesis: verum