let L be non empty right_complementable add-associative right_zeroed left-distributive unital doubleLoopStr ; for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)
let z0, z1, x be Element of L; eval (<%z0,z1%>,x) = z0 + (z1 * x)
consider F being FinSequence of the carrier of L such that
A1:
eval (<%z0,z1%>,x) = Sum F
and
A2:
len F = len <%z0,z1%>
and
A3:
for n being Element of NAT st n in dom F holds
F . n = (<%z0,z1%> . (n -' 1)) * ((power L) . (x,(n -' 1)))
by POLYNOM4:def 2;
len F <= 2
by A2, Th39;
then
not not len F = 0 & ... & not len F = 2
;
per cases then
( len F = 0 or len F = 1 or len F = 2 )
;
suppose A5:
len F = 1
;
eval (<%z0,z1%>,x) = z0 + (z1 * x)then
0 + 1
in Seg (len F)
by FINSEQ_1:4;
then
1
in dom F
by FINSEQ_1:def 3;
then F . 1 =
(<%z0,z1%> . (1 -' 1)) * ((power L) . (x,(1 -' 1)))
by A3
.=
(<%z0,z1%> . 0) * ((power L) . (x,(1 -' 1)))
by XREAL_1:232
.=
(<%z0,z1%> . 0) * ((power L) . (x,0))
by XREAL_1:232
.=
z0 * ((power L) . (x,0))
by Th38
.=
z0 * (1_ L)
by GROUP_1:def 7
.=
z0
by GROUP_1:def 4
;
then
F = <*z0*>
by A5, FINSEQ_1:40;
hence eval (
<%z0,z1%>,
x) =
z0
by A1, RLVECT_1:44
.=
z0 + (0. L)
by RLVECT_1:def 4
.=
z0 + ((0. L) * x)
.=
z0 + ((<%z0,z1%> . 1) * x)
by A2, A5, ALGSEQ_1:8
.=
z0 + (z1 * x)
by Th38
;
verum end; suppose A6:
len F = 2
;
eval (<%z0,z1%>,x) = z0 + (z1 * x)then
1
in dom F
by FINSEQ_3:25;
then A7:
F . 1 =
(<%z0,z1%> . (1 -' 1)) * ((power L) . (x,(1 -' 1)))
by A3
.=
(<%z0,z1%> . 0) * ((power L) . (x,(1 -' 1)))
by XREAL_1:232
.=
(<%z0,z1%> . 0) * ((power L) . (x,0))
by XREAL_1:232
.=
z0 * ((power L) . (x,0))
by Th38
.=
z0 * (1_ L)
by GROUP_1:def 7
.=
z0
by GROUP_1:def 4
;
A8:
2
-' 1
= 2
- 1
by XREAL_0:def 2;
2
in dom F
by A6, FINSEQ_3:25;
then F . 2 =
(<%z0,z1%> . (2 -' 1)) * ((power L) . (x,(2 -' 1)))
by A3
.=
z1 * ((power L) . (x,1))
by A8, Th38
.=
z1 * x
by GROUP_1:50
;
then
F = <*z0,(z1 * x)*>
by A6, A7, FINSEQ_1:44;
hence
eval (
<%z0,z1%>,
x)
= z0 + (z1 * x)
by A1, RLVECT_1:45;
verum end;