let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis:
let z be rational_function of L; :: thesis:
let x be Element of L; :: thesis:

suppose A: not z is zero ; :: thesis:

then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A1: ( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF z = NormRatF z1 & 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) ) ) ) ) by defNF;
consider f being FinSequence of (Polynom-Ring L) such that
A2: ( 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 A1;
set q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))];

assume [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ; :: thesis:
then (rpoly (1,x)) *' (z `1) = 0_. L ;
then z `1 = 0_. L by tt2;
hence contradiction by A, defzerrat; :: thesis:

end;

then reconsider q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] as non zero rational_function of L by defzerrat;
reconsider rp = rpoly (1,x) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
set g = <*rp*> ^ f;
reconsider g = <*rp*> ^ f as FinSequence of (Polynom-Ring L) ;
set g2 = Product g;

let i be Nat; :: thesis:
assume Y: i in dom g ; :: thesis:

per cases by Y, FINSEQ_1:25;

suppose X: i in dom <*rp*> ; :: thesis:

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
then g . i = <*rp*> . 1 by X, FINSEQ_1:def 7
.= rp by FINSEQ_1:40 ;
hence ex z being Element of L st g . i = rpoly (1,z) ; :: thesis:

end;

suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; :: thesis:

then consider n being Nat such that
H: ( n in dom f & i = (len <*rp*>) + n ) ;
J: g . i = f . n by H, FINSEQ_1:def 7;
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,x) ) by H, A2;
hence ex z being Element of L st g . i = rpoly (1,z) by J; :: thesis:

end;

end;

end;

hence ex z being Element of L st g . i = rpoly (1,z) ; :: thesis:

end;

then Product g <> 0_. L by div4;
then reconsider g2 = Product g as non zero Polynomial of L by defzer, POLYNOM3:def 10;

A3: now :: thesis:

let i be Element of NAT ; :: thesis:
assume Y: i in dom g ; :: thesis:

per cases by Y, FINSEQ_1:25;

suppose X: i in dom <*rp*> ; :: thesis:

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
then I: g . i = <*rp*> . 1 by X, FINSEQ_1:def 7
.= rp by FINSEQ_1:40 ;
H: eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
then 0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `1),x)) by VECTSP_1:7
.= eval (((rpoly (1,x)) *' (z `1)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def 6;
then J: x is_a_root_of q `1 by XTUPLE_0:def 2;
0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `2),x)) by H, VECTSP_1:7
.= eval (((rpoly (1,x)) *' (z `2)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def 6;
then x is_a_root_of q `2 by XTUPLE_0:def 3;
then x is_a_common_root_of q `1 ,q `2 by J, root1;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by I; :: thesis:

end;

suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; :: thesis:

then consider n being Nat such that
H: ( n in dom f & i = (len <*rp*>) + n ) ;
J: g . i = f . n by H, FINSEQ_1:def 7;
consider y being Element of L such that
I: ( y is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,y) ) by H, A2;
y is_a_root_of z `1 by I, root1;
then eval ((z `1),y) = 0. L by POLYNOM5:def 6;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `1),y)) by VECTSP_1:6
.= eval (((rpoly (1,x)) *' (z `1)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def 6;
then K: y is_a_root_of q `1 by XTUPLE_0:def 2;
y is_a_root_of z `2 by I, root1;
then eval ((z `2),y) = 0. L by POLYNOM5:def 6;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `2),y)) by VECTSP_1:6
.= eval (((rpoly (1,x)) *' (z `2)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def 6;
then y is_a_root_of q `2 by XTUPLE_0:def 3;
then y is_a_common_root_of q `1 ,q `2 by K, root1;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by J, I; :: thesis:

end;

end;

end;

hence ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) ; :: thesis:

end;

A4: Product g = rp * (Product f) by GROUP_4:7;
A5: q `1 = (rpoly (1,x)) *' (z `1) by XTUPLE_0:def 2
.= (rpoly (1,x)) *' (z2 *' (z1 `1)) by A1, XTUPLE_0:def 2
.= ((rpoly (1,x)) *' z2) *' (z1 `1) by POLYNOM3:33
.= g2 *' (z1 `1) by A4, A2, POLYNOM3:def 10 ;
q `2 = (rpoly (1,x)) *' (z `2) by XTUPLE_0:def 3
.= (rpoly (1,x)) *' (z2 *' (z1 `2)) by A1, XTUPLE_0:def 3
.= ((rpoly (1,x)) *' z2) *' (z1 `2) by POLYNOM3:33
.= g2 *' (z1 `2) by A4, A2, POLYNOM3:def 10 ;
then q = [(g2 *' (z1 `1)),(g2 *' (z1 `2))] by A5, ttt;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A1, A3, defNF; :: thesis:

end;

suppose A: z is zero ; :: thesis:

then z `1 = 0_. L by defzerrat;
then (rpoly (1,x)) *' (z `1) = 0_. L by POLYNOM3:34;
then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 = 0_. L ;
then [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] is zero by defzerrat;
then NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = 0._ L by defNF;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A, defNF; :: thesis:

end;

end;