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

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