let L be non empty right_complementable right-distributive add-associative right_zeroed unital associative commutative 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 A1: 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 Nat such that
A2: ( ii = i & 1 <= ii & ii <= len f ) ;
reconsider j = i - 1 as Element of NAT by A2, INT_1:5;
set g = Del (f,i);
thus Product f = Product (Ins ((Del (f,i)),j,(f /. i))) by A1, Th2
.= (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