let S be non empty finite set ; for X being Subset of S
for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)
let X be Subset of S; for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)
let s, t be FinSequence of S; for SD being Subset of (dom s)
for x being set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)
let SD be Subset of (dom s); for x being set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)
let x be set ; ( SD = s " X & t = extract (s,SD) & x in X implies frequency (x,s) = frequency (x,t) )
assume A1:
( SD = s " X & t = extract (s,SD) & x in X )
; frequency (x,s) = frequency (x,t)
then
for a being object st a in {x} holds
a in X
by TARSKI:def 1;
then
{x} is Subset of X
by TARSKI:def 3;
hence
frequency (x,s) = frequency (x,t)
by Th34, A1; verum