let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L holds even_part (p + q) = (even_part p) + (even_part q)
let p, q be Polynomial of L; :: thesis: even_part (p + q) = (even_part p) + (even_part q)
set epq = even_part (p + q);
set ep = even_part p;
set eq = even_part q;
A1: dom (even_part (p + q)) = NAT by FUNCT_2:def 1
.= dom ((even_part p) + (even_part q)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (even_part (p + q)) holds
((even_part p) + (even_part q)) . x = (even_part (p + q)) . x

let x be object ; :: thesis: ( x in dom (even_part (p + q)) implies ((even_part p) + (even_part q)) . x = (even_part (p + q)) . x )
assume x in dom (even_part (p + q)) ; :: thesis: ((even_part p) + (even_part q)) . x = (even_part (p + q)) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;

now :: thesis: ( ( i is even & ((even_part p) + (even_part q)) . i = (even_part (p + q)) . i ) or ( i is odd & ((even_part p) + (even_part q)) . i = (even_part (p + q)) . i ) )

per cases ( i is even or i is odd ) ;

case A2: i is even ; :: thesis: ((even_part p) + (even_part q)) . i = (even_part (p + q)) . i

thus ((even_part p) + (even_part q)) . i = ((even_part p) . i) + ((even_part q) . i) by NORMSP_1:def 2
.= (p . i) + ((even_part q) . i) by A2, Def1
.= (p . i) + (q . i) by A2, Def1
.= (p + q) . i by NORMSP_1:def 2
.= (even_part (p + q)) . i by A2, Def1 ; :: thesis: verum

end;

case A3: i is odd ; :: thesis: ((even_part p) + (even_part q)) . i = (even_part (p + q)) . i

thus ((even_part p) + (even_part q)) . i = ((even_part p) . i) + ((even_part q) . i) by NORMSP_1:def 2
.= (0. L) + ((even_part q) . i) by A3, Def1
.= (0. L) + (0. L) by A3, Def1
.= 0. L by RLVECT_1:def 4
.= (even_part (p + q)) . i by A3, Def1 ; :: thesis: verum

end;

end;

end;

hence ((even_part p) + (even_part q)) . x = (even_part (p + q)) . x ; :: thesis: verum

end;

hence even_part (p + q) = (even_part p) + (even_part q) by A1, FUNCT_1:2; :: thesis: verum