let F be Field; :: thesis: for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2
let S1, S2 be non empty finite Subset of F; :: thesis: for p1 being Ppoly of F,S1
for p2 being Polynomial of F st S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2
let p1 be Ppoly of F,S1; :: thesis: for p2 being Polynomial of F st S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2
let p2 be Polynomial of F; :: thesis: ( S2 = S1 /\ (Roots p2) implies p1 gcd p2 is Ppoly of F,S2 )
assume AS: S2 = S1 /\ (Roots p2) ; :: thesis: p1 gcd p2 is Ppoly of F,S2
defpred S₁[ Nat] means for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st card S2 = $1 & S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2;
A: S₁[ 0 ] ;
B: S₁[1]

proof

now :: thesis: for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st card S2 = 1 & S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2

let S1, S2 be non empty finite Subset of F; :: thesis: for p1 being Ppoly of F,S1
for p2 being Polynomial of F st card S2 = 1 & S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2
let p1 be Ppoly of F,S1; :: thesis: for p2 being Polynomial of F st card S2 = 1 & S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2
let p2 be Polynomial of F; :: thesis: ( card S2 = 1 & S2 = S1 /\ (Roots p2) implies p1 gcd p2 is Ppoly of F,S2 )
assume B1: ( card S2 = 1 & S2 = S1 /\ (Roots p2) ) ; :: thesis: p1 gcd p2 is Ppoly of F,S2
then consider a being object such that
B2: S2 = {a} by CARD_2:42;
a in {a} by TARSKI:def 1;
then reconsider a = a as Element of F by B2;
set q = rpoly (1,a);
B3: rpoly (1,a) divides p1

proof

C1: Roots p1 = S1 by RING_5:63;
a in S2 by B2, TARSKI:def 1;
then a in Roots p1 by B1, C1, XBOOLE_0:def 4;
then a is_a_root_of p1 by POLYNOM5:def 10;
then consider s being Polynomial of F such that
C2: p1 = (rpoly (1,a)) *' s by HURWITZ:33;
thus rpoly (1,a) divides p1 by C2, RING_4:1; :: thesis: verum

end;

B4: rpoly (1,a) divides p2

proof

a in S2 by B2, TARSKI:def 1;
then a in Roots p2 by B1, XBOOLE_0:def 4;
then a is_a_root_of p2 by POLYNOM5:def 10;
then consider s being Polynomial of F such that
C2: p2 = (rpoly (1,a)) *' s by HURWITZ:33;
thus rpoly (1,a) divides p2 by C2, RING_4:1; :: thesis: verum

end;

now :: thesis: for r being Polynomial of F st r divides p2 & r divides p1 holds
r divides rpoly (1,a)

let r be Polynomial of F; :: thesis: ( r divides p2 & r divides p1 implies b₁ divides rpoly (1,a) )
assume C1: ( r divides p2 & r divides p1 ) ; :: thesis: b₁ divides rpoly (1,a)
consider s1 being Polynomial of F such that
F1: p1 = r *' s1 by C1, RING_4:1;
consider s2 being Polynomial of F such that
F2: p2 = r *' s2 by C1, RING_4:1;

per cases ( r is constant or not r is constant ) ;

suppose r is constant ; :: thesis: b₁ divides rpoly (1,a)

then deg r <= 0 by RATFUNC1:def 2;
then reconsider r1 = r as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
consider b being Element of F such that
C2: r1 = b | F by RING_4:20;
C3: r = b * (1_. F) by C2, RING_4:16;
C4: b <> 0. F by F1, C2;
(b * (1_. F)) *' ((b ") * (rpoly (1,a))) = (b ") * ((b * (1_. F)) *' (rpoly (1,a))) by RING_4:10
.= (b ") * (b * ((1_. F) *' (rpoly (1,a)))) by RING_4:10
.= ((b ") * b) * ((1_. F) *' (rpoly (1,a))) by RING_4:11
.= (1. F) * (rpoly (1,a)) by C4, VECTSP_1:def 10
.= rpoly (1,a) ;
hence r divides rpoly (1,a) by C3, RING_4:1; :: thesis: verum

end;

suppose not r is constant ; :: thesis: b₁ divides rpoly (1,a)

then G6: deg r > 0 by RATFUNC1:def 2;
then reconsider r1 = r as non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
set r1N = NormPolynomial r1;
G4: r1 <> 0_. F ;
then G1: ( len r1 <> 0 & LC r <> 0. F ) by POLYNOM4:5;
len r1 = len (NormPolynomial r1) by G4, POLYNOM5:57, POLYNOM4:5;
then deg (NormPolynomial r1) = (len r1) - 1 by HURWITZ:def 2
.= deg r by HURWITZ:def 2 ;
then reconsider r1Np = NormPolynomial r1 as non constant monic Polynomial of F by G6, RATFUNC1:def 2;
G5: r1Np = ((LC r1) ") * r by RING_4:23;
r1Np *' ((LC r) * s1) = (LC r) * (r1Np *' s1) by RING_4:10
.= ((LC r) * (((LC r1) ") * r)) *' s1 by G5, RING_4:10
.= (((LC r) * ((LC r1) ")) * r) *' s1 by RING_4:11
.= ((1. F) * r) *' s1 by G1, VECTSP_1:def 10
.= p1 by F1 ;
then consider S3 being non empty finite Subset of F such that
C2: ( r1Np is Ppoly of F,S3 & S3 c= S1 ) by RING_4:1, simpAgcd1;
G2: r1Np *' ((LC r) * s2) = (LC r) * (r1Np *' s2) by RING_4:10
.= ((LC r) * (((LC r1) ") * r)) *' s2 by G5, RING_4:10
.= (((LC r) * ((LC r1) ")) * r) *' s2 by RING_4:11
.= ((1. F) * r) *' s2 by G1, VECTSP_1:def 10
.= p2 by F2 ;

now :: thesis: not S3 <> {a}

assume H: S3 <> {a} ; :: thesis: contradiction

now :: thesis: a in S3

assume D0: not a in S3 ; :: thesis: contradiction
consider b being Element of F such that
D1: b is_a_root_of r1Np by C2, POLYNOM5:def 8;
b is_a_root_of r1 by G1, D1, POLYNOM5:59;
then b is_a_root_of p1 by F1, ro1;
then b in Roots p1 by POLYNOM5:def 10;
then E: b in S1 by RING_5:63;
b is_a_root_of p2 by G2, D1, ro1;
then b in Roots p2 by POLYNOM5:def 10;
then D2: b in S2 by B1, E;
b in Roots r1Np by D1, POLYNOM5:def 10;
then b <> a by D0, C2, RING_5:63;
hence contradiction by D2, B2, TARSKI:def 1; :: thesis: verum

end;

then C6: {a} c= S3 by TARSKI:def 1;

now :: thesis: ex b being Element of F st
( b in S3 & b <> a )

assume G: for b being Element of F holds
( not b in S3 or not b <> a ) ; :: thesis: contradiction

now :: thesis: for o being object st o in S3 holds
o in {a}

let o be object ; :: thesis: ( o in S3 implies o in {a} )
assume J: o in S3 ; :: thesis: o in {a}
then reconsider c = o as Element of F ;
c = a by G, J;
hence o in {a} by TARSKI:def 1; :: thesis: verum

end;

then S3 c= {a} ;
hence contradiction by H, C6; :: thesis: verum

end;

then consider b being Element of F such that
C3: ( b in S3 & b <> a ) ;
not b in S2 by B2, C3, TARSKI:def 1;
then not b in Roots p2 by C2, C3, B1;
then C5: not b is_a_root_of p2 by POLYNOM5:def 10;

now :: thesis: not r1Np divides p2

assume r1Np divides p2 ; :: thesis: contradiction
then consider s being Polynomial of F such that
C6: p2 = r1Np *' s by RING_4:1;
eval (r1Np,b) = 0. F by C2, C3, RING_5:62;
then eval (p2,b) = (0. F) * (eval (s,b)) by C6, POLYNOM4:24
.= 0. F ;
hence contradiction by C5, POLYNOM5:def 7; :: thesis: verum

end;

hence contradiction by G2, RING_4:1; :: thesis: verum

end;

then C9: rpoly (1,a) = (1_. F) *' r1Np by C2, simpAgcd2;
r *' (((LC r) ") * (1_. F)) = ((LC r) ") * (r *' (1_. F)) by RING_4:10
.= rpoly (1,a) by RING_4:23, C9 ;
hence r divides rpoly (1,a) by RING_4:1; :: thesis: verum

end;

end;

end;

then rpoly (1,a) = p1 gcd p2 by B3, B4, RING_4:53;
hence p1 gcd p2 is Ppoly of F,S2 by B2, RING_5:57; :: thesis: verum

end;

hence S₁[1] ; :: thesis: verum

end;

C: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume D0: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for S1, S2 being non empty finite Subset of F
for p1 being Ppoly of F,S1
for p2 being Polynomial of F st card S2 = k + 1 & S2 = S1 /\ (Roots p2) holds
p1 gcd p2 is Ppoly of F,S2

let S1, S2 be non empty finite Subset of F; :: thesis: for p1 being Ppoly of F,S1
for p2 being Polynomial of F st card S2 = k + 1 & S2 = S1 /\ (Roots p2) holds
b₅ gcd b₆ is Ppoly of F,b₄
let p1 be Ppoly of F,S1; :: thesis: for p2 being Polynomial of F st card S2 = k + 1 & S2 = S1 /\ (Roots p2) holds
b₄ gcd b₅ is Ppoly of F,b₃
let p2 be Polynomial of F; :: thesis: ( card S2 = k + 1 & S2 = S1 /\ (Roots p2) implies b₃ gcd b₄ is Ppoly of F,b₂ )
assume D1: ( card S2 = k + 1 & S2 = S1 /\ (Roots p2) ) ; :: thesis: b₃ gcd b₄ is Ppoly of F,b₂
set a = the Element of S2;
D2: ( the Element of S2 in S1 & the Element of S2 in Roots p2 ) by D1, XBOOLE_0:def 4;
reconsider S3 = S2 \ { the Element of S2} as finite Subset of F ;

now :: thesis: for o being object st o in { the Element of S2} holds
o in S2

let o be object ; :: thesis: ( o in { the Element of S2} implies o in S2 )
assume o in { the Element of S2} ; :: thesis: o in S2
then o = the Element of S2 by TARSKI:def 1;
hence o in S2 ; :: thesis: verum

end;

then D6: { the Element of S2} c= S2 ;
then D3: S2 = S3 \/ { the Element of S2} by XBOOLE_1:45;
the Element of S2 in { the Element of S2} by TARSKI:def 1;
then not the Element of S2 in S3 by XBOOLE_0:def 5;
then D4: card S2 = (card S3) + 1 by D3, CARD_2:41;

per cases ( S3 is empty or not S3 is empty ) ;

suppose S3 is empty ; :: thesis: b₃ gcd b₄ is Ppoly of F,b₂

hence p1 gcd p2 is Ppoly of F,S2 by B, D1, D4; :: thesis: verum

end;

suppose not S3 is empty ; :: thesis: b₃ gcd b₄ is Ppoly of F,b₂

then reconsider S3 = S3 as non empty finite Subset of F ;

now :: thesis: not S1 \ { the Element of S2} is empty

assume D5: S1 \ { the Element of S2} is empty ; :: thesis: contradiction
I: S1 = { the Element of S2}

proof

now :: thesis: for o being object st o in { the Element of S2} holds
o in S1

let o be object ; :: thesis: ( o in { the Element of S2} implies o in S1 )
assume o in { the Element of S2} ; :: thesis: o in S1
then o = the Element of S2 by TARSKI:def 1;
hence o in S1 by D1, XBOOLE_0:def 4; :: thesis: verum

end;

then D6: { the Element of S2} c= S1 ;

now :: thesis: for o being object st o in S1 holds
o in { the Element of S2}

let o be object ; :: thesis: ( o in S1 implies o in { the Element of S2} )
assume H: o in S1 ; :: thesis: o in { the Element of S2}
then reconsider b = o as Element of F ;

now :: thesis: not b <> the Element of S2

assume b <> the Element of S2 ; :: thesis: contradiction
then not b in { the Element of S2} by TARSKI:def 1;
hence contradiction by D5, H, XBOOLE_0:def 5; :: thesis: verum

end;

hence o in { the Element of S2} by TARSKI:def 1; :: thesis: verum

end;

then S1 c= { the Element of S2} ;
hence S1 = { the Element of S2} by D6; :: thesis: verum

end;

S2 = { the Element of S2}

proof

S2 c= { the Element of S2} by I, D1, XBOOLE_0:def 4;
hence S2 = { the Element of S2} by D6; :: thesis: verum

end;

then card S2 = 1 by CARD_2:42;
then card S3 = 0 by D4;
hence contradiction ; :: thesis: verum

end;

then reconsider S4 = S1 \ { the Element of S2} as non empty finite Subset of F ;
{ the Element of S2} c= S1 by D2, TARSKI:def 1;
then E1: S1 = S4 \/ { the Element of S2} by XBOOLE_1:45;
Roots p1 = S1 by RING_5:63;
then the Element of S2 is_a_root_of p1 by D2, POLYNOM5:def 10;
then consider p1a being Polynomial of F such that
D5: p1 = (rpoly (1, the Element of S2)) *' p1a by HURWITZ:33;

now :: thesis: not p1a is constant

assume p1a is constant ; :: thesis: contradiction
then deg p1a <= 0 by RATFUNC1:def 2;
then reconsider r = p1a as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
consider b being Element of F such that
D6: r = b | F by RING_4:20;
1. F = LC p1a by D5, ZZ3y, RATFUNC1:def 7
.= b by D6, RING_5:6 ;
then p1a = 1_. F by D6, RING_4:14;
then { the Element of S2} = Roots p1 by D5, RING_5:18
.= S1 by RING_5:63 ;
then S1 \ ({ the Element of S2} \/ {}) = {} by XBOOLE_1:46;
then S4 is empty ;
hence contradiction ; :: thesis: verum

end;

then reconsider p1a = p1a as Ppoly of F,S4 by D5, r59;
the Element of S2 is_a_root_of p2 by D2, POLYNOM5:def 10;
then consider p2a being Polynomial of F such that
D6: p2 = (rpoly (1, the Element of S2)) *' p2a by HURWITZ:33;

per cases ( S4 /\ (Roots p2a) is empty or not S4 /\ (Roots p2a) is empty ) ;

suppose E0: S4 /\ (Roots p2a) is empty ; :: thesis: b₃ gcd b₄ is Ppoly of F,b₂

S4 = Roots p1a by RING_5:63;
then E2: p1a gcd p2a = 1_. F by E0, ZZ3;
E4: Roots (rpoly (1, the Element of S2)) = { the Element of S2} by RING_5:18;
E3: S2 = (S4 \/ { the Element of S2}) /\ ({ the Element of S2} \/ (Roots p2a)) by D1, E1, E4, D6, UPROOTS:23
.= (S4 /\ (Roots p2a)) \/ { the Element of S2} by XBOOLE_1:24
.= { the Element of S2} by E0 ;
p1 gcd p2 = (rpoly (1, the Element of S2)) *' (1_. F) by E2, D5, D6, ZZ2;
hence p1 gcd p2 is Ppoly of F,S2 by E3, RING_5:57; :: thesis: verum

end;

suppose not S4 /\ (Roots p2a) is empty ; :: thesis: b₃ gcd b₄ is Ppoly of F,b₂

then reconsider S5 = S4 /\ (Roots p2a) as non empty finite Subset of F ;
E2: Roots (rpoly (1, the Element of S2)) = { the Element of S2} by RING_5:18;
the Element of S2 in { the Element of S2} by TARSKI:def 1;
then not the Element of S2 in S4 by XBOOLE_0:def 5;
then E3: not the Element of S2 in S5 by XBOOLE_0:def 4;

D10: now :: thesis: not { the Element of S2} /\ S5 <> {}

assume F1: { the Element of S2} /\ S5 <> {} ; :: thesis: contradiction
set o = the Element of { the Element of S2} /\ S5;
( the Element of { the Element of S2} /\ S5 in { the Element of S2} & the Element of { the Element of S2} /\ S5 in S5 ) by F1, XBOOLE_0:def 4;
then the Element of S2 in S4 /\ (Roots p2a) by TARSKI:def 1;
then the Element of S2 in S4 by XBOOLE_0:def 4;
then not the Element of S2 in { the Element of S2} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

D9: { the Element of S2} \/ S5 = ({ the Element of S2} \/ S4) /\ ({ the Element of S2} \/ (Roots p2a)) by XBOOLE_1:24
.= S2 by D1, E1, E2, D6, UPROOTS:23 ;
then k + 1 = (card S5) + 1 by D1, E3, CARD_2:41;
then D7: p1a gcd p2a is Ppoly of F,S5 by D0;
D8: p1 gcd p2 = (rpoly (1, the Element of S2)) *' (p1a gcd p2a) by D5, D6, ZZ2;
rpoly (1, the Element of S2) is Ppoly of F,{ the Element of S2} by RING_5:57;
hence p1 gcd p2 is Ppoly of F,S2 by D10, D9, D7, D8, r58; :: thesis: verum

end;

end;

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, C);
consider n being Nat such that
H: card S2 = n ;
thus p1 gcd p2 is Ppoly of F,S2 by AS, I, H; :: thesis: verum