let L be comRing; :: thesis: for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f = len z holds
for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))
let z be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence st len f = len z holds
for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))
let f be NAT -valued FinSequence; :: thesis: ( len f = len z implies for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp)) )
assume A1: len f = len z ; :: thesis: for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))
let p be Permutation of (dom f); :: thesis: for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))
let zp be FinSequence of the carrier of L; :: thesis: ( zp = z * p implies Product (rpoly (f,z)) = Product (rpoly ((f * p),zp)) )
assume A2: zp = z * p ; :: thesis: Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))
len f = len (rpoly (f,z)) by Def1;
then A3: dom f = dom (rpoly (f,z)) by FINSEQ_3:29;
rpoly ((f * p),zp) = (rpoly (f,z)) * p by A1, A2, Th47;
hence Product (rpoly (f,z)) = Product (rpoly ((f * p),zp)) by A3, UPROOTS:16; :: thesis: verum