let p be Prime; :: thesis: for n being non empty Element of NAT holds p |-count <*n*> = <*(p |-count n)*>
let n be non empty 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:56 ;
Seg 1 = Seg (len <*(p |-count n)*>) by FINSEQ_1:56;
then A2: dom (p |-count <*n*>) = dom <*(p |-count n)*> by A1, FINSEQ_1:def 3;
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 A4: (p |-count <*n*>) . k = p |-count (<*n*> . k) by Def1;
( 1 <= k & k <= 1 ) by A1, A3, FINSEQ_1:3;
then A5: k = 1 by XXREAL_0:1;
then (p |-count <*n*>) . k = p |-count n by A4, FINSEQ_1:57;
hence (p |-count <*n*>) . k = <*(p |-count n)*> . k by A5, FINSEQ_1:57; :: thesis: verum

end;

hence p |-count <*n*> = <*(p |-count n)*> by A2, FINSEQ_1:17; :: thesis: verum