:: deftheorem Def14 defines ConditionalSS DIST_2:def 14 :
for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D
for b₄ being EqSampleSpaces of S holds
( b₄ = ConditionalSS X iff ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in b₄ ) );