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 ) )
set x = s . n;
assume n in dom s ; :: thesis: ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
then s . n in rng s by FUNCT_1:3;
then s . n in S ;
then s . n in rng (canFS S) by FUNCT_2:def 3;
then consider m being object such that
A1: m in dom (canFS S) and
A2: s . n = (canFS S) . m by FUNCT_1:def 3;
reconsider m = m as Nat by A1;
take m ; :: thesis: ( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
Seg (len (canFS S)) = Seg (card S) by FINSEQ_1:93;
then dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
then ex xx being Element of S st
( (freqSEQ s) . m = frequency (xx,s) & xx = (canFS S) . m ) by A1, Th11;
hence ( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m ) by A2; :: thesis: verum