let L be non empty ZeroStr ; :: thesis: ( even_part (0_. L) = 0_. L & odd_part (0_. L) = 0_. L )
set e = even_part (0_. L);
set p = 0_. L;
A1: dom (0_. L) = NAT by FUNCT_2:def 1
.= dom (even_part (0_. L)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (0_. L) holds
(0_. L) . x = (even_part (0_. L)) . x

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

now :: thesis: ( ( i is even & (even_part (0_. L)) . i = (0_. L) . i ) or ( i is odd & (even_part (0_. L)) . i = (0_. L) . i ) )

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

case i is even ; :: thesis: (even_part (0_. L)) . i = (0_. L) . i

hence (even_part (0_. L)) . i = (0_. L) . i by Def1; :: thesis: verum

end;

case i is odd ; :: thesis: (even_part (0_. L)) . i = (0_. L) . i

hence (even_part (0_. L)) . i = 0. L by Def1
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum

end;

end;

end;

hence (0_. L) . x = (even_part (0_. L)) . x ; :: thesis: verum

end;

hence even_part (0_. L) = 0_. L by A1, FUNCT_1:2; :: thesis: odd_part (0_. L) = 0_. L
set o = odd_part (0_. L);
A2: dom (0_. L) = NAT by FUNCT_2:def 1
.= dom (odd_part (0_. L)) by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom (0_. L) holds
(0_. L) . x = (odd_part (0_. L)) . x

let x be object ; :: thesis: ( x in dom (0_. L) implies (0_. L) . x = (odd_part (0_. L)) . x )
assume x in dom (0_. L) ; :: thesis: (0_. L) . x = (odd_part (0_. L)) . x
then reconsider i = x as Element of NAT by FUNCT_2:def 1;

now :: thesis: ( ( i is odd & (odd_part (0_. L)) . i = (0_. L) . i ) or ( i is even & (odd_part (0_. L)) . i = (0_. L) . i ) )

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

case i is odd ; :: thesis: (odd_part (0_. L)) . i = (0_. L) . i

hence (odd_part (0_. L)) . i = (0_. L) . i by Def2; :: thesis: verum

end;

case i is even ; :: thesis: (odd_part (0_. L)) . i = (0_. L) . i

hence (odd_part (0_. L)) . i = 0. L by Def2
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum

end;

end;

end;

hence (0_. L) . x = (odd_part (0_. L)) . x ; :: thesis: verum

end;

hence odd_part (0_. L) = 0_. L by A2, FUNCT_1:2; :: thesis: verum