let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for z being non zero rational_function of L holds
( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )
let z be non zero rational_function of L; :: thesis: ( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )
set q = z `2 ;
set a = (LC (z `2)) " ;

now :: thesis: not (LC (z `2)) " = 0. L

assume AB: (LC (z `2)) " = 0. L ; :: thesis: contradiction
then AC: ((LC (z `2)) ") * (LC (z `2)) = 0. L by VECTSP_1:7;
(LC (z `2)) " <> 1. L by AB;
hence contradiction by AC, VECTSP_1:def 10; :: thesis: verum

end;

then reconsider a = (LC (z `2)) " as non zero Element of L by STRUCT_0:def 12;
reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L ;

A: now :: thesis: ( z is irreducible implies ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) )

assume z is irreducible ; :: thesis: ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z )
then NF z = NormRatF z by defnf1a
.= [(((1. L) / (LC (z `2))) * (z `1)),(((1. L) / (LC (z `2))) * (z `2))] ;
hence ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; :: thesis: verum

end;

now :: thesis: ( ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) implies z is irreducible )

assume ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ; :: thesis: z is irreducible
then consider a being Element of L such that
H0: ( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ;
reconsider x = [(a * (z `1)),(a * (z `2))] as rational_function of L by H0;
H1: ( x `1 = a * (z `1) & x `2 = a * (z `2) ) by XTUPLE_0:def 2, XTUPLE_0:def 3;

now :: thesis: not z `1 ,z `2 have_a_common_root

assume z `1 ,z `2 have_a_common_root ; :: thesis: contradiction
then consider u being Element of L such that
C1: u is_a_common_root_of z `1 ,z `2 by root2;
( u is_a_root_of z `1 & u is_a_root_of z `2 ) by root1, C1;
then C3: ( eval ((z `1),u) = 0. L & eval ((z `2),u) = 0. L ) by POLYNOM5:def 6;
eval ((x `1),u) = a * (eval ((z `1),u)) by H1, POLYNOM5:30;
then eval ((x `1),u) = 0. L by C3, VECTSP_1:6;
then C2: u is_a_root_of x `1 by POLYNOM5:def 6;
eval ((x `2),u) = a * (eval ((z `2),u)) by H1, POLYNOM5:30;
then eval ((x `2),u) = 0. L by C3, VECTSP_1:7;
then u is_a_root_of x `2 by POLYNOM5:def 6;
then u is_a_common_root_of x `1 ,x `2 by C2, root1;
then x `1 ,x `2 have_a_common_root by root2;
hence contradiction by defirred, H0; :: thesis: verum

end;

hence z is irreducible by defirred; :: thesis: verum

end;

hence ( z is irreducible iff ex a being Element of L st
( a <> 0. L & [(a * (z `1)),(a * (z `2))] = NF z ) ) by A; :: thesis: verum