consider x being sample of D such that
A1: x in X by Def12;
consider s being Element of D such that
A2: x in rng s by Def10;
consider n being object such that
A3: n in dom s and
A4: x = s . n by A2, FUNCT_1:def 3;
reconsider SD = s " X as Subset of (dom s) by RELAT_1:132;
reconsider t = extract (s,SD) as FinSequence of S ;
reconsider DX = Finseq-EQclass t as Element of distribution_family S by DIST_1:def 6;
A5: t in DX ;
n in SD by A3, A4, A1, FUNCT_1:def 7;
then card SD <> 0 ;
then len t <> 0 by Th11;
then t <> <*> S ;
then not DX = {(<*> S)} by A5, TARSKI:def 1;
then reconsider DX = DX as EqSampleSpaces of S by Th6;
take DX ; :: thesis: 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 DX )
thus 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 DX ) by A5; :: thesis: verum