let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for z1, z2 being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f <= len z1 & len f <= len z2 & z1 | (len f) = z2 | (len f) holds
rpoly (f,z1) = rpoly (f,z2)
let z1, z2 be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence st len f <= len z1 & len f <= len z2 & z1 | (len f) = z2 | (len f) holds
rpoly (f,z1) = rpoly (f,z2)
let f be NAT -valued FinSequence; :: thesis: ( len f <= len z1 & len f <= len z2 & z1 | (len f) = z2 | (len f) implies rpoly (f,z1) = rpoly (f,z2) )
assume A1: ( len f <= len z1 & len f <= len z2 & z1 | (len f) = z2 | (len f) ) ; :: thesis: rpoly (f,z1) = rpoly (f,z2)
A2: ( len (rpoly (f,z1)) = len f & len f = len (rpoly (f,z2)) ) by Def1;
for i being Nat st 1 <= i & i <= len f holds
(rpoly (f,z1)) . i = (rpoly (f,z2)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies (rpoly (f,z1)) . i = (rpoly (f,z2)) . i )
assume A3: ( 1 <= i & i <= len f ) ; :: thesis: (rpoly (f,z1)) . i = (rpoly (f,z2)) . i
( len (z1 | (len f)) = len f & len f = len (z2 | (len f)) ) by A1, FINSEQ_1:59;
then ( i in dom (z1 | (len f)) & dom (z1 | (len f)) c= dom z1 & i in dom (z2 | (len f)) & dom (z2 | (len f)) c= dom z2 ) by A3, FINSEQ_3:25, RELAT_1:60;
then ( (z1 | (len f)) . i = z1 . i & z1 . i = z1 /. i & (z2 | (len f)) . i = z2 . i & z2 . i = z2 /. i ) by PARTFUN1:def 6, FUNCT_1:47;
hence (rpoly (f,z1)) . i = rpoly ((f /. i),(z2 /. i)) by A1, A3, Def1
.= (rpoly (f,z2)) . i by A3, Def1 ;
:: thesis: verum

end;

hence rpoly (f,z1) = rpoly (f,z2) by A2, FINSEQ_1:14; :: thesis: verum