let L be non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A1: (LC (z `2)) " = 0. L ; :: thesis: contradiction
then A2: ((LC (z `2)) ") * (LC (z `2)) = 0. L ;
(LC (z `2)) " <> 1. L by A1;
hence contradiction by A2, 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 ;

A3: 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 Lm4
.= [(((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
A4: ( 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 A4;

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
A5: u is_a_common_root_of z `1 ,z `2 ;
( u is_a_root_of z `1 & u is_a_root_of z `2 ) by A5;
then A6: ( eval ((z `1),u) = 0. L & eval ((z `2),u) = 0. L ) by POLYNOM5:def 7;
eval ((x `1),u) = a * (eval ((z `1),u)) by POLYNOM5:30;
then eval ((x `1),u) = 0. L by A6;
then A7: u is_a_root_of x `1 by POLYNOM5:def 7;
eval ((x `2),u) = a * (eval ((z `2),u)) by POLYNOM5:30;
then eval ((x `2),u) = 0. L by A6;
then u is_a_root_of x `2 by POLYNOM5:def 7;
then u is_a_common_root_of x `1 ,x `2 by A7;
then x `1 ,x `2 have_a_common_root ;
hence contradiction by Def10, A4; :: thesis: verum

end;

hence z is irreducible ; :: 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 A3; :: thesis: verum