let p be Prime; :: thesis: for n being non zero Element of NAT holds p |-count <*n*> = <*(p |-count n)*>
let n be non zero Element of NAT ; :: thesis: p |-count <*n*> = <*(p |-count n)*>
A1: dom (p |-count <*n*>) = Seg (len (p |-count <*n*>)) by FINSEQ_1:def 3
.= Seg (len <*n*>) by Def1
.= Seg 1 by FINSEQ_1:39 ;
A2: for k being Nat st k in dom (p |-count <*n*>) holds
(p |-count <*n*>) . k = <*(p |-count n)*> . k

proof

let k be Nat; :: thesis: ( k in dom (p |-count <*n*>) implies (p |-count <*n*>) . k = <*(p |-count n)*> . k )
assume A3: k in dom (p |-count <*n*>) ; :: thesis: (p |-count <*n*>) . k = <*(p |-count n)*> . k
then ( 1 <= k & k <= 1 ) by A1, FINSEQ_1:1;
then A4: k = 1 by XXREAL_0:1;
(p |-count <*n*>) . k = p |-count (<*n*> . k) by A3, Def1;
then (p |-count <*n*>) . k = p |-count n by A4;
hence (p |-count <*n*>) . k = <*(p |-count n)*> . k by A4; :: thesis: verum

end;

Seg 1 = Seg (len <*(p |-count n)*>) by FINSEQ_1:39;
then dom (p |-count <*n*>) = dom <*(p |-count n)*> by A1, FINSEQ_1:def 3;
hence p |-count <*n*> = <*(p |-count n)*> by A2, FINSEQ_1:13; :: thesis: verum