let g, h be FinSequence of NAT ; :: thesis: ( len g = len f & ( for i being set st i in dom g holds
g . i = p |-count (f . i) ) & len h = len f & ( for i being set st i in dom h holds
h . i = p |-count (f . i) ) implies g = h )
assume that
A5: len g = len f and
A6: for i being set st i in dom g holds
g . i = p |-count (f . i) and
A7: len h = len f and
A8: for i being set st i in dom h holds
h . i = p |-count (f . i) ; :: thesis: g = h
A9: ( dom g = Seg (len g) & dom h = Seg (len h) ) by FINSEQ_1:def 3;
for k being Nat st k in dom g holds
g . k = h . k

proof

let k be Nat; :: thesis: ( k in dom g implies g . k = h . k )
assume A10: k in dom g ; :: thesis: g . k = h . k
hence g . k = p |-count (f . k) by A6
.= h . k by A5, A7, A8, A9, A10 ;
:: thesis: verum

end;

hence g = h by A5, A7, A9, FINSEQ_1:13; :: thesis: verum