let S be non empty finite set ; :: thesis: for s being non empty FinSequence of S
for n being Nat st n in dom s holds
ex m being Nat st
( () . m = frequency ((s . n),s) & s . n = () . m )

let s be non empty FinSequence of S; :: thesis: for n being Nat st n in dom s holds
ex m being Nat st
( () . m = frequency ((s . n),s) & s . n = () . m )

let n be Nat; :: thesis: ( n in dom s implies ex m being Nat st
( () . m = frequency ((s . n),s) & s . n = () . m ) )

set x = s . n;
assume n in dom s ; :: thesis: ex m being Nat st
( () . m = frequency ((s . n),s) & s . n = () . m )

then s . n in rng s by FUNCT_1:3;
then s . n in S ;
then s . n in rng () by FUNCT_2:def 3;
then consider m being object such that
A1: m in dom () and
A2: s . n = () . m by FUNCT_1:def 3;
reconsider m = m as Nat by A1;
take m ; :: thesis: ( () . m = frequency ((s . n),s) & s . n = () . m )
Seg (len ()) = Seg (card S) by FINSEQ_1:93;
then dom () = Seg (card S) by FINSEQ_1:def 3;
then ex xx being Element of S st
( () . m = frequency (xx,s) & xx = () . m ) by ;
hence ( (freqSEQ s) . m = frequency ((s . n),s) & s . n = () . m ) by A2; :: thesis: verum