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
( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . 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
( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . m )
let n be Nat; :: thesis: ( n in dom s implies ex m being Nat st
( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . m ) )
assume AS: n in dom s ; :: thesis: ex m being Nat st
( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . m )
set x = s . n;
s . n in rng s by FUNCT_1:12, AS;
then s . n in S ;
then s . n in rng (canFS S) by FUNCT_2:def 3;
then consider m being set such that
DM: ( m in dom (canFS S) & s . n = (canFS S) . m ) by FUNCT_1:def 5;
reconsider m = m as Nat by DM;
Seg (len (canFS S)) = Seg (card S) by UPROOTS:5;
then J1P: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
consider xx being Element of S such that
J2: ( (freqSEQ s) . m = frequency xx,s & xx = (canFS S) . m ) by nazonazo, J1P, DM;
take m ; :: thesis: ( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . m )
thus ( (freqSEQ s) . m = frequency (s . n),s & s . n = (canFS S) . m ) by DM, J2; :: thesis: verum