let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: 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
rpoly ((f * p),zp) = (rpoly (f,z)) * p
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
rpoly ((f * p),zp) = (rpoly (f,z)) * p
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
rpoly ((f * p),zp) = (rpoly (f,z)) * p )
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
rpoly ((f * p),zp) = (rpoly (f,z)) * p
let p be Permutation of (dom f); :: thesis: for zp being FinSequence of the carrier of L st zp = z * p holds
rpoly ((f * p),zp) = (rpoly (f,z)) * p
let zp be FinSequence of the carrier of L; :: thesis: ( zp = z * p implies rpoly ((f * p),zp) = (rpoly (f,z)) * p )
assume A2: zp = z * p ; :: thesis: rpoly ((f * p),zp) = (rpoly (f,z)) * p
A3: dom (f * p) = dom f by NEWTON04:9;
len (rpoly ((f * p),zp)) = len (f * p) by Def1;
then A4: dom (rpoly ((f * p),zp)) = dom (f * p) by FINSEQ_3:29;
A5: len (rpoly (f,z)) = len f by Def1;
then dom (rpoly (f,z)) = dom f by FINSEQ_3:29;
then A6: dom ((rpoly (f,z)) * p) = dom f by NEWTON04:9;
for x being object st x in dom f holds
(rpoly ((f * p),zp)) . x = ((rpoly (f,z)) * p) . x

proof

let x be object ; :: thesis: ( x in dom f implies (rpoly ((f * p),zp)) . x = ((rpoly (f,z)) * p) . x )
assume A7: x in dom f ; :: thesis: (rpoly ((f * p),zp)) . x = ((rpoly (f,z)) * p) . x
reconsider i = x as Nat by A7;
( 1 <= i & i <= len f & i <= len (f * p) ) by A7, A3, FINSEQ_3:25;
then A8: (rpoly ((f * p),zp)) . x = rpoly (((f * p) /. i),(zp /. i)) by Def1;
A9: ( ((rpoly (f,z)) * p) . x = (rpoly (f,z)) . (p . x) & p . x in dom (rpoly (f,z)) ) by A7, A6, FUNCT_1:11, FUNCT_1:12;
then ( 1 <= p . x & p . x <= len f ) by A5, FINSEQ_3:25;
then A10: (rpoly (f,z)) . (p . x) = rpoly ((f /. (p . x)),(z /. (p . x))) by Def1;
A11: ( (f * p) /. i = (f * p) . i & (f * p) . i = f . (p . i) & p . x in dom f ) by A7, A3, PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;
then A12: f /. (p . x) = f . (p . x) by PARTFUN1:def 6;
A13: dom f = dom z by A1, FINSEQ_3:29;
then dom zp = dom z by A2, NEWTON04:9;
then ( zp /. i = zp . i & zp . i = z . (p . i) & p . i in dom z ) by A2, A7, A13, PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;
hence (rpoly ((f * p),zp)) . x = ((rpoly (f,z)) * p) . x by A8, A9, A10, A11, A12, PARTFUN1:def 6; :: thesis: verum

end;

hence rpoly ((f * p),zp) = (rpoly (f,z)) * p by A3, A4, A6, FUNCT_1:2; :: thesis: verum