set R = Z/ 6;

set z = 2 '*' (1. (Z/ 6));

set d = 3 '*' (1. (Z/ 6));

take p = rpoly (1,(2 '*' (1. (Z/ 6)))); :: thesis: not for q being Polynomial of (Z/ 6) holds Roots (p *' q) c= (Roots p) \/ (Roots q)

take q = rpoly (1,(3 '*' (1. (Z/ 6)))); :: thesis: not Roots (p *' q) c= (Roots p) \/ (Roots q)

C: Char (Z/ 6) = 6 by RING_3:77;

eval ((p *' q),(0. (Z/ 6))) = (eval (p,(0. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by POLYNOM4:24

.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by HURWITZ:29

.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by HURWITZ:29

.= (- (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by RLVECT_1:14

.= (- (2 '*' (1. (Z/ 6)))) * (- (3 '*' (1. (Z/ 6)))) by RLVECT_1:14

.= (2 '*' (1. (Z/ 6))) * (3 '*' (1. (Z/ 6))) by VECTSP_1:10

.= (2 * 3) '*' (1. (Z/ 6)) by RING_3:67

.= 0. (Z/ 6) by C, RING_3:def 5 ;

then 0. (Z/ 6) is_a_root_of p *' q by POLYNOM5:def 7;

then B: 0. (Z/ 6) in Roots (p *' q) by POLYNOM5:def 10;

set z = 2 '*' (1. (Z/ 6));

set d = 3 '*' (1. (Z/ 6));

take p = rpoly (1,(2 '*' (1. (Z/ 6)))); :: thesis: not for q being Polynomial of (Z/ 6) holds Roots (p *' q) c= (Roots p) \/ (Roots q)

take q = rpoly (1,(3 '*' (1. (Z/ 6)))); :: thesis: not Roots (p *' q) c= (Roots p) \/ (Roots q)

C: Char (Z/ 6) = 6 by RING_3:77;

eval ((p *' q),(0. (Z/ 6))) = (eval (p,(0. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by POLYNOM4:24

.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by HURWITZ:29

.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by HURWITZ:29

.= (- (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by RLVECT_1:14

.= (- (2 '*' (1. (Z/ 6)))) * (- (3 '*' (1. (Z/ 6)))) by RLVECT_1:14

.= (2 '*' (1. (Z/ 6))) * (3 '*' (1. (Z/ 6))) by VECTSP_1:10

.= (2 * 3) '*' (1. (Z/ 6)) by RING_3:67

.= 0. (Z/ 6) by C, RING_3:def 5 ;

then 0. (Z/ 6) is_a_root_of p *' q by POLYNOM5:def 7;

then B: 0. (Z/ 6) in Roots (p *' q) by POLYNOM5:def 10;

now :: thesis: not 0. (Z/ 6) in (Roots p) \/ (Roots q)

hence
not Roots (p *' q) c= (Roots p) \/ (Roots q)
by B; :: thesis: verumassume AS:
0. (Z/ 6) in (Roots p) \/ (Roots q)
; :: thesis: contradiction

end;per cases
( 0. (Z/ 6) in Roots p or 0. (Z/ 6) in Roots q )
by AS, XBOOLE_0:def 3;

end;

suppose
0. (Z/ 6) in Roots p
; :: thesis: contradiction

then
0. (Z/ 6) is_a_root_of p
by POLYNOM5:def 10;

then B: 0. (Z/ 6) = eval (p,(0. (Z/ 6))) by POLYNOM5:def 7

.= (0. (Z/ 6)) - (2 '*' (1. (Z/ 6))) by HURWITZ:29

.= - (2 '*' (1. (Z/ 6))) by RLVECT_1:14 ;

2 '*' (1. (Z/ 6)) = - (- (2 '*' (1. (Z/ 6))))

.= 0. (Z/ 6) by B ;

hence contradiction by C, RING_3:def 5; :: thesis: verum

end;then B: 0. (Z/ 6) = eval (p,(0. (Z/ 6))) by POLYNOM5:def 7

.= (0. (Z/ 6)) - (2 '*' (1. (Z/ 6))) by HURWITZ:29

.= - (2 '*' (1. (Z/ 6))) by RLVECT_1:14 ;

2 '*' (1. (Z/ 6)) = - (- (2 '*' (1. (Z/ 6))))

.= 0. (Z/ 6) by B ;

hence contradiction by C, RING_3:def 5; :: thesis: verum

suppose
0. (Z/ 6) in Roots q
; :: thesis: contradiction

then
0. (Z/ 6) is_a_root_of q
by POLYNOM5:def 10;

then B: 0. (Z/ 6) = eval (q,(0. (Z/ 6))) by POLYNOM5:def 7

.= (0. (Z/ 6)) - (3 '*' (1. (Z/ 6))) by HURWITZ:29

.= - (3 '*' (1. (Z/ 6))) by RLVECT_1:14 ;

3 '*' (1. (Z/ 6)) = - (- (3 '*' (1. (Z/ 6))))

.= 0. (Z/ 6) by B ;

hence contradiction by C, RING_3:def 5; :: thesis: verum

end;then B: 0. (Z/ 6) = eval (q,(0. (Z/ 6))) by POLYNOM5:def 7

.= (0. (Z/ 6)) - (3 '*' (1. (Z/ 6))) by HURWITZ:29

.= - (3 '*' (1. (Z/ 6))) by RLVECT_1:14 ;

3 '*' (1. (Z/ 6)) = - (- (3 '*' (1. (Z/ 6))))

.= 0. (Z/ 6) by B ;

hence contradiction by C, RING_3:def 5; :: thesis: verum