let s be Nat; for k, w being non zero Nat st k <= s & w <= s & w <> k holds
((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w
let k, w be non zero Nat; ( k <= s & w <= s & w <> k implies ((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w )
assume that
A1:
k <= s
and
A2:
w <= s
and
A3:
w <> k
; ((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w
A4:
1 <= w
by NAT_1:14;
set p = primenumber (k - 1);
set AnPk = sequenceAnPk (s,k);
len (sequenceAnPk (s,k)) = s
by A1, Def10;
then reconsider AnPk = sequenceAnPk (s,k) as s -element natural-valued FinSequence by CARD_1:def 7;
set I = idseq s;
set A = sequenceA s;
set f = (idseq s) to_power (sequenceA s);
set F = (idseq s) to_power AnPk;
A5:
len (((idseq s) to_power AnPk) |^ (primenumber (k - 1))) = len ((idseq s) to_power AnPk)
by NAT_3:def 1;
A6:
len ((idseq s) to_power AnPk) = s
by CARD_1:def 7;
then A7:
w in dom (((idseq s) to_power AnPk) |^ (primenumber (k - 1)))
by A2, A4, A5, FINSEQ_3:25;
A8:
w in Seg s
by A2, A4;
then A9:
(idseq s) . w = w
by FINSEQ_2:49;
dom ((idseq s) to_power AnPk) = Seg s
by A6, FINSEQ_1:def 3;
then A10:
((idseq s) to_power AnPk) . w = ((idseq s) . w) to_power (AnPk . w)
by A8, Def6;
A11:
AnPk . w = ((sequenceA s) . w) / (primenumber (k - 1))
by A1, A2, A3, Def10;
len ((idseq s) to_power (sequenceA s)) = s
by CARD_1:def 7;
then
w in dom ((idseq s) to_power (sequenceA s))
by A2, A4, FINSEQ_3:25;
then ((idseq s) to_power (sequenceA s)) . w =
((idseq s) . w) to_power ((sequenceA s) . w)
by Def6
.=
w |^ ((AnPk . w) * (primenumber (k - 1)))
by A9, A11, XCMPLX_1:87
.=
(((idseq s) to_power AnPk) . w) |^ (primenumber (k - 1))
by A9, A10, NEWTON:9
.=
(((idseq s) to_power AnPk) |^ (primenumber (k - 1))) . w
by A7, NAT_3:def 1
;
hence
((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w
; verum