let R be non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr ; :: thesis: for p being sequence of R holds (1_. R) *' p = p
let p be sequence of R; :: thesis: (1_. R) *' p = p
set q = 1_. R;
now :: thesis: for x being object st x in NAT holds
((1_. R) *' p) . x = p . x
let x be object ; :: thesis: ( x in NAT implies ((1_. R) *' p) . x = p . x )
assume x in NAT ; :: thesis: ((1_. R) *' p) . x = p . x
then reconsider i = x as Element of NAT ;
consider F being FinSequence of the carrier of R such that
H: ( len F = i + 1 & ((1_. R) *' p) . i = Sum F & ( for k being Element of NAT st k in dom F holds
F . k = ((1_. R) . (k -' 1)) * (p . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
D: now :: thesis: for j being Element of NAT st j in dom F & j <> 1 holds
0. R = F /. j
let j be Element of NAT ; :: thesis: ( j in dom F & j <> 1 implies 0. R = F /. j )
assume B: ( j in dom F & j <> 1 ) ; :: thesis: 0. R = F /. j
then j in Seg (len F) by FINSEQ_1:def 3;
then ( 1 <= j & j <= i + 1 ) by H, FINSEQ_1:1;
then j > 1 by B, XXREAL_0:1;
then (1_. R) . (j -' 1) = 0. R by POLYNOM3:30, NAT_D:36;
hence 0. R = ((1_. R) . (j -' 1)) * (p . ((i + 1) -' j))
.= F . j by B, H
.= F /. j by B, PARTFUN1:def 6 ;
:: thesis: verum
end;
G: dom F = Seg (i + 1) by H, FINSEQ_1:def 3;
E: ( 1 <= 1 & 1 <= i + 1 ) by NAT_1:11;
then F: Sum F = F /. 1 by D, POLYNOM2:3, G, FINSEQ_1:1;
F . 1 = ((1_. R) . (1 -' 1)) * (p . ((i + 1) -' 1)) by H, E, G, FINSEQ_1:1
.= ((1_. R) . 0) * (p . ((i + 1) -' 1)) by XREAL_1:232
.= ((1_. R) . 0) * (p . i) by NAT_D:34
.= (1. R) * (p . i) by POLYNOM3:30
.= p . i ;
hence ((1_. R) *' p) . x = p . x by E, H, F, PARTFUN1:def 6, G, FINSEQ_1:1; :: thesis: verum
end;
hence (1_. R) *' p = p by FUNCT_2:12; :: thesis: verum