let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A1: 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 A2: ( 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 A3: ( 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
A4: ( 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 A2;

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 A5: dom f <> {} ;
let i be Element of dom f; :: thesis: contradiction
reconsider i = i as Nat ;
A6: i in dom f by A5;
consider x being Element of L such that
A7: ( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) by A6, A4;
z `1 ,z `2 have_common_roots by A7;
hence contradiction by A1; :: thesis: verum

end;

hence A8: z2 = 1_ (Polynom-Ring L) by A4, GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
:: thesis: ( g2 = 1_. L & z1 = g1 )
then A9: z2 *' (z1 `1) = z1 `1 by POLYNOM3:35;
z2 *' (z1 `2) = z1 `2 by A8, POLYNOM3:35;
then A10: z = z1 by A9, A2, Th19;
consider h being FinSequence of (Polynom-Ring L) such that
A11: ( 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 A3;

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 A12: dom h <> {} ;
let i be Element of dom h; :: thesis: contradiction
reconsider i = i as Nat ;
A13: i in dom h by A12;
consider x being Element of L such that
A14: ( x is_a_common_root_of z `1 ,z `2 & h . i = rpoly (1,x) ) by A13, A11;
z `1 ,z `2 have_common_roots by A14;
hence contradiction by A1; :: thesis: verum

end;

hence A15: g2 = 1_ (Polynom-Ring L) by A11, GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
:: thesis: z1 = g1
then A16: g2 *' (g1 `1) = g1 `1 by POLYNOM3:35;
g2 *' (g1 `2) = g1 `2 by A15, POLYNOM3:35;
hence z1 = g1 by A10, A16, A3, Th19; :: thesis: verum