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

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

end;

now

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

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 A3;
then A7: k <= 1 by NAT_1:13;

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

suppose A8: 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 A8, VECTSP_1:def 13 ;
:: thesis: verum

end;

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

then A9: 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 A5, VECTSP_1:def 22
.= p . k by A9, VECTSP_1:def 19 ;
:: thesis: verum

end;

end;

end;

then p = (p . 1) * (rpoly 1,((- (p . 0 )) * ((p . 1) " ))) by A6, ALGSEQ_1:28;
hence ex x, z being Element of L st
( x <> 0. L & p = x * (rpoly 1,z) ) by A4, ALGSEQ_1:25; :: 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