let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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

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:25;

A5: now

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 3
.= (p . 1) * (1_ L) by Lm11
.= p . k by A7, VECTSP_1:def 13 ;
:: 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 3
.= (p . 1) * (- ((power L) . ((- (p . 0 )) * ((p . 1) " )),(1 + 0 ))) by Lm11
.= (p . 1) * (- (((power L) . ((- (p . 0 )) * ((p . 1) " )),0 ) * ((- (p . 0 )) * ((p . 1) " )))) by GROUP_1:def 8
.= (p . 1) * (- ((1_ L) * ((- (p . 0 )) * ((p . 1) " )))) by GROUP_1:def 8
.= (p . 1) * (- ((- (p . 0 )) * ((p . 1) " ))) by VECTSP_1:def 19
.= (p . 1) * (- (- ((p . 0 ) * ((p . 1) " )))) by VECTSP_1:41
.= (p . 1) * ((p . 0 ) * ((p . 1) " )) by RLVECT_1:30
.= ((p . 1) * ((p . 1) " )) * (p . 0 ) by GROUP_1:def 4
.= (1_ L) * (p . 0 ) by A4, VECTSP_1:def 22
.= p . k by A8, VECTSP_1:def 19 ;
:: 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:25, POLYNOM5:26
.= 1 + 1 by Th27
.= len p by A2 ;
then p = (p . 1) * (rpoly 1,((- (p . 0 )) * ((p . 1) " ))) by A5, ALGSEQ_1:28;
hence ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly 1,z) ) by A3, ALGSEQ_1:25; :: thesis: verum

end;

now

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:26
.= 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