let DX1, DX2 be EqSampleSpaces of S; :: 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 DX1 ) & 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 DX2 ) implies DX1 = DX2 )
given s1 being Element of D, t1 being FinSequence of S, SD1 being Subset of (dom s1) such that A6: ( SD1 = s1 " X & t1 = extract (s1,SD1) & t1 in DX1 ) ; :: thesis: ( for s being Element of D
for t being FinSequence of S
for SD being Subset of (dom s) holds
( not SD = s " X or not t = extract (s,SD) or not t in DX2 ) or DX1 = DX2 )
given s2 being Element of D, t2 being FinSequence of S, SD2 being Subset of (dom s2) such that A7: ( SD2 = s2 " X & t2 = extract (s2,SD2) & t2 in DX2 ) ; :: thesis: DX1 = DX2
( DX1 = Finseq-EQclass t1 & DX2 = Finseq-EQclass t2 ) by Th36, A6, A7;
hence DX1 = DX2 by DIST_1:9, A6, A7, Th38; :: thesis: verum