let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L holds
( deg p = 1 iff ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) )
let p be Polynomial of L; :: thesis: ( deg p = 1 iff ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) )

A1: now :: thesis: ( deg p = 1 implies ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) )

set x = p . 1;
set z = (- (p . 0)) * ((p . 1) ");
set f = (p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))));
assume A2: deg p = 1 ; :: thesis: ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) )
then A3: len p = 1 + 1 ;
then A4: p . 1 <> 0. L by ALGSEQ_1:10;

A5: now :: thesis: for k being Nat st k < len p holds
((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . k = p . k

let k be Nat; :: thesis: ( k < len p implies ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b₁ = p . b₁ )
assume k < len p ; :: thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b₁ = p . b₁
then k < 1 + 1 by A2;
then A6: k <= 1 by NAT_1:13;

per cases ( k = 1 or k < 1 ) by A6, XXREAL_0:1;

suppose A7: k = 1 ; :: thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b₁ = p . b₁

hence ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . k = (p . 1) * ((rpoly (1,((- (p . 0)) * ((p . 1) ")))) . 1) by POLYNOM5:def 4
.= (p . 1) * (1_ L) by Lm10
.= p . k by A7 ;
:: thesis: verum

end;

suppose k < 1 ; :: thesis: ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . b₁ = p . b₁

then A8: k = 0 by NAT_1:14;
hence ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) . k = (p . 1) * ((rpoly (1,((- (p . 0)) * ((p . 1) ")))) . 0) by POLYNOM5:def 4
.= (p . 1) * (- ((power L) . (((- (p . 0)) * ((p . 1) ")),(1 + 0)))) by Lm10
.= (p . 1) * (- (((power L) . (((- (p . 0)) * ((p . 1) ")),0)) * ((- (p . 0)) * ((p . 1) ")))) by GROUP_1:def 7
.= (p . 1) * (- ((1_ L) * ((- (p . 0)) * ((p . 1) ")))) by GROUP_1:def 7
.= (p . 1) * (- ((- (p . 0)) * ((p . 1) ")))
.= (p . 1) * (- (- ((p . 0) * ((p . 1) ")))) by VECTSP_1:9
.= (p . 1) * ((p . 0) * ((p . 1) ")) by RLVECT_1:17
.= ((p . 1) * ((p . 1) ")) * (p . 0) by GROUP_1:def 3
.= (1_ L) * (p . 0) by A4, VECTSP_1:def 10
.= p . k by A8 ;
:: thesis: verum

end;

end;

end;

len ((p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) "))))) = (deg (rpoly (1,((- (p . 0)) * ((p . 1) "))))) + 1 by A3, ALGSEQ_1:10, POLYNOM5:25
.= 1 + 1 by Th27
.= len p by A2 ;
then p = (p . 1) * (rpoly (1,((- (p . 0)) * ((p . 1) ")))) by A5, ALGSEQ_1:12;
hence ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) by A3, ALGSEQ_1:10; :: thesis: verum

end;

now :: thesis: ( ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) implies deg p = 1 )

given x, z being Element of L such that A9: x <> 0. L and
A10: p = x * (rpoly (1,z)) ; :: thesis: deg p = 1
thus deg p = deg (rpoly (1,z)) by A9, A10, POLYNOM5:25
.= 1 by Th27 ; :: thesis: verum

end;

hence ( deg p = 1 iff ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly (1,z)) ) ) by A1; :: thesis: verum