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 :: thesis: for x being object st x in Support p holds
x in Support ((Up (p,T,i)) + (Low (p,T,i)))

let x be object ; :: 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:15;

A5: now :: thesis: ( ( x9 in Support (Up (p,T,i)) & ((Up (p,T,i)) + (Low (p,T,i))) . x9 = p . x9 ) or ( x9 in Support (Low (p,T,i)) & ((Up (p,T,i)) + (Low (p,T,i))) . x9 = p . x9 ) )

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 4
.= 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 2
.= p . x9 by A1, A7, Th31 ;
:: thesis: verum

end;

end;

end;

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

end;

now :: thesis: for x being object st x in Support ((Up (p,T,i)) + (Low (p,T,i))) holds
x in Support p

let x be object ; :: 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:20, XBOOLE_1:8;
then A8: Support ((Up (p,T,i)) + (Low (p,T,i))) c= Support p ;
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 :: thesis: for x being object st x in dom p holds
p . x = ((Up (p,T,i)) + (Low (p,T,i))) . x

let x be object ; :: 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:15;

now :: thesis: ( ( x9 in Support p & p . x9 = ((Up (p,T,i)) + (Low (p,T,i))) . x9 ) or ( not x9 in Support p & p . x9 = ((Up (p,T,i)) + (Low (p,T,i))) . x9 ) )

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 :: thesis: ( ( x9 in Support (Up (p,T,i)) & ((Up (p,T,i)) + (Low (p,T,i))) . x9 = p . x9 ) or ( x9 in Support (Low (p,T,i)) & ((Up (p,T,i)) + (Low (p,T,i))) . x9 = p . x9 ) )

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 4
.= 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 2
.= 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 4
.= ((Up (p,T,i)) + (Low (p,T,i))) . x9 by A9, A15, POLYNOM1:def 4 ;
:: 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:2; :: thesis: verum