let S be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum