let L be non empty right_complementable unital associative commutative right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being FinSequence of L
for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))
let f be FinSequence of L; :: thesis: for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))
let i be Element of NAT ; :: thesis: ( i in dom f implies Product f = (f /. i) * (Product (Del (f,i))) )
assume AS: i in dom f ; :: thesis: Product f = (f /. i) * (Product (Del (f,i)))
then i in Seg (len f) by FINSEQ_1:def 3;
then consider ii being Element of NAT such that
H: ( ii = i & 1 <= ii & ii <= len f ) ;
reconsider j = i - 1 as Element of NAT by H, INT_1:5;
set g = Del (f,i);
thus Product f = Product (Ins ((Del (f,i)),j,(f /. i))) by AS, del1a
.= (Product (((Del (f,i)) | j) ^ <*(f /. i)*>)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:5
.= ((Product ((Del (f,i)) | j)) * (f /. i)) * (Product ((Del (f,i)) /^ j)) by GROUP_4:6
.= (f /. i) * ((Product ((Del (f,i)) | j)) * (Product ((Del (f,i)) /^ j))) by GROUP_1:def 3
.= (f /. i) * (Product (((Del (f,i)) | j) ^ ((Del (f,i)) /^ j))) by GROUP_4:5
.= (f /. i) * (Product (Del (f,i))) by RFINSEQ:8 ; :: thesis: verum