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
for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
let z be rational_function of L; :: thesis: for x being Element of L holds NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z
let x be Element of L; :: thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z

per cases ( not z is zero or z is zero ) ;

suppose A1: not z is zero ; :: thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z

then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A2: ( 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 Def17;
consider f being FinSequence of (Polynom-Ring L) such that
A3: ( 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;
set q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))];
[((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] `1 <> 0_. L by A1, Lm5;
then reconsider q = [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] as non zero rational_function of L by Def9;
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;

now :: thesis: for i being Nat st i in dom g holds
ex z being Element of L st g . i = rpoly (1,z)

let i be Nat; :: thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume A4: i in dom g ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)

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

per cases ( i in dom <*rp*> or ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ) by A4, FINSEQ_1:25;

suppose A5: i in dom <*rp*> ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)

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

end;

suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)

then consider n being Nat such that
A6: ( n in dom f & i = (len <*rp*>) + n ) ;
A7: g . i = f . n by A6, 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 A6, A3;
hence ex z being Element of L st g . i = rpoly (1,z) by A7; :: thesis: verum

end;

end;

end;

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

end;

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

A8: now :: thesis: for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) )

let i be Element of NAT ; :: thesis: ( i in dom g implies ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) ) )
assume A9: i in dom g ; :: thesis: ex x being Element of L st
( x is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,x) )

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

per cases ( i in dom <*rp*> or ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ) by A9, FINSEQ_1:25;

suppose A10: i in dom <*rp*> ; :: thesis: ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) )

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
then A11: g . i = <*rp*> . 1 by A10, FINSEQ_1:def 7
.= rp ;
A12: 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))
.= eval (((rpoly (1,x)) *' (z `1)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def 7;
then A13: x is_a_root_of q `1 ;
0. L = (eval ((rpoly (1,x)),x)) * (eval ((z `2),x)) by A12
.= eval (((rpoly (1,x)) *' (z `2)),x) by POLYNOM4:24 ;
then x is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def 7;
then x is_a_root_of q `2 ;
then x is_a_common_root_of q `1 ,q `2 by A13;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by A11; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom f & i = (len <*rp*>) + n ) ; :: thesis: ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) )

then consider n being Nat such that
A14: ( n in dom f & i = (len <*rp*>) + n ) ;
A15: g . i = f . n by A14, FINSEQ_1:def 7;
consider y being Element of L such that
A16: ( y is_a_common_root_of z `1 ,z `2 & f . n = rpoly (1,y) ) by A14, A3;
y is_a_root_of z `1 by A16;
then eval ((z `1),y) = 0. L by POLYNOM5:def 7;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `1),y))
.= eval (((rpoly (1,x)) *' (z `1)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `1) by POLYNOM5:def 7;
then A17: y is_a_root_of q `1 ;
y is_a_root_of z `2 by A16;
then eval ((z `2),y) = 0. L by POLYNOM5:def 7;
then 0. L = (eval ((rpoly (1,x)),y)) * (eval ((z `2),y))
.= eval (((rpoly (1,x)) *' (z `2)),y) by POLYNOM4:24 ;
then y is_a_root_of (rpoly (1,x)) *' (z `2) by POLYNOM5:def 7;
then y is_a_root_of q `2 ;
then y is_a_common_root_of q `1 ,q `2 by A17;
hence ex z being Element of L st
( z is_a_common_root_of q `1 ,q `2 & g . i = rpoly (1,z) ) by A15, A16; :: thesis: verum

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: verum

end;

A18: Product g = rp * (Product f) by GROUP_4:7;
A19: q `1 = (rpoly (1,x)) *' (z `1)
.= (rpoly (1,x)) *' (z2 *' (z1 `1)) by A2
.= ((rpoly (1,x)) *' z2) *' (z1 `1) by POLYNOM3:33
.= g2 *' (z1 `1) by A18, A3, POLYNOM3:def 10 ;
q `2 = (rpoly (1,x)) *' (z `2)
.= (rpoly (1,x)) *' (z2 *' (z1 `2)) by A2
.= ((rpoly (1,x)) *' z2) *' (z1 `2) by POLYNOM3:33
.= g2 *' (z1 `2) by A18, A3, POLYNOM3:def 10 ;
then q = [(g2 *' (z1 `1)),(g2 *' (z1 `2))] by A19;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A2, A8, Def17; :: thesis: verum

end;

suppose A20: z is zero ; :: thesis: NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z

then z `1 = 0_. L ;
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 ;
then NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = 0._ L by Def17;
hence NF [((rpoly (1,x)) *' (z `1)),((rpoly (1,x)) *' (z `2))] = NF z by A20, Def17; :: thesis: verum

end;

end;