let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for z being rational_function of L st z is irreducible holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z be rational_function of L; :: thesis: ( z is irreducible implies for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume AS: z is irreducible ; :: thesis: for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z1 be rational_function of L; :: thesis: for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let z2 be non zero Polynomial of L; :: thesis: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume A: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; :: thesis: for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let g1 be rational_function of L; :: thesis: for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
let g2 be non zero Polynomial of L; :: thesis: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) implies ( z2 = 1_. L & g2 = 1_. L & z1 = g1 ) )
assume B: ( z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ; :: thesis: ( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
consider f being FinSequence of (Polynom-Ring L) such that
C: ( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by A;

now :: thesis: ( f <> <*> the carrier of (Polynom-Ring L) implies for i being Element of dom f holds contradiction )

assume f <> <*> the carrier of (Polynom-Ring L) ; :: thesis: for i being Element of dom f holds contradiction
then G: dom f <> {} ;
let i be Element of dom f; :: thesis: contradiction
reconsider i = i as Nat ;
D1: i in dom f by G;
consider x being Element of L such that
D2: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by D1, C;
z `1 ,z `2 have_common_roots by D2, root2;
hence contradiction by AS, defirred; :: thesis: verum

end;

hence D2: z2 = 1_ (Polynom-Ring L) by C, GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
:: thesis: ( g2 = 1_. L & z1 = g1 )
then D1: z2 *' (z1 `1) = z1 `1 by POLYNOM3:35;
z2 *' (z1 `2) = z1 `2 by D2, POLYNOM3:35;
then D: z = z1 by D1, A, ttt;
consider h being FinSequence of (Polynom-Ring L) such that
E: ( g2 = Product h & ( for i being Element of NAT st i in dom h holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) ) ) by B;

now :: thesis: ( h <> <*> the carrier of (Polynom-Ring L) implies for i being Element of dom h holds contradiction )

assume h <> <*> the carrier of (Polynom-Ring L) ; :: thesis: for i being Element of dom h holds contradiction
then G: dom h <> {} ;
let i be Element of dom h; :: thesis: contradiction
reconsider i = i as Nat ;
D1: i in dom h by G;
consider x being Element of L such that
D2: ( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) by D1, E;
z `1 ,z `2 have_common_roots by D2, root2;
hence contradiction by AS, defirred; :: thesis: verum

end;

hence E2: g2 = 1_ (Polynom-Ring L) by E, GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
:: thesis: z1 = g1
then E1: g2 *' (g1 `1) = g1 `1 by POLYNOM3:35;
g2 *' (g1 `2) = g1 `2 by E2, POLYNOM3:35;
hence z1 = g1 by D, E1, B, ttt; :: thesis: verum