let SOURCE be non empty finite set ; :: thesis: for p being Probability of Trivial-SigmaField SOURCE holds card (Initial-Trees p) = card SOURCE
let p be Probability of Trivial-SigmaField SOURCE; :: thesis: card (Initial-Trees p) = card SOURCE
set L = { T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;
reconsider fcs = (canFS SOURCE) " as Function of SOURCE,(Seg (card SOURCE)) by FINSEQ_1:95;
len (canFS SOURCE) = card SOURCE by FINSEQ_1:93;
then ( dom (canFS SOURCE) = Seg (card SOURCE) & rng (canFS SOURCE) = SOURCE ) by FINSEQ_1:def 3, FUNCT_2:def 3;
then reconsider g = canFS SOURCE as Function of (Seg (card SOURCE)),SOURCE by FUNCT_2:1;
defpred S2[ object , object ] means $2 = root-tree [(fcs . $1),(p . {$1})];
A1: for x being object st x in SOURCE holds
ex y being object st
( y in Initial-Trees p & S2[x,y] )
proof
let x be object ; :: thesis: ( x in SOURCE implies ex y being object st
( y in Initial-Trees p & S2[x,y] ) )
assume A2: x in SOURCE ; :: thesis: ex y being object st
( y in Initial-Trees p & S2[x,y] )
then reconsider x0 = x as Element of SOURCE ;
A3: fcs . x in Seg (card SOURCE) by A2, FUNCT_2:5;
p . {x0} in REAL ;
then A4: [(fcs . x),(p . {x})] in [:NAT,REAL:] by A3, ZFMISC_1:87;
take T = root-tree [(fcs . x),(p . {x})]; :: thesis: ( T in Initial-Trees p & S2[x,T] )
dom T = elementary_tree 0 ;
then T is Element of FinTrees IndexedREAL by A4, TREES_3:def 8;
hence ( T in Initial-Trees p & S2[x,T] ) by A4, A2; :: thesis: verum
end;
consider f being Function of SOURCE,(Initial-Trees p) such that
A5: for x being object st x in SOURCE holds
S2[x,f . x] from FUNCT_2:sch 1(A1);
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A6: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then A7: ( x1 in SOURCE & x2 in SOURCE ) ;
A8: f . x1 = root-tree [(fcs . x1),(p . {x1})] by A5, A6;
A9: f . x2 = root-tree [(fcs . x2),(p . {x2})] by A5, A6;
A10: f . x1 in Initial-Trees p by A6, FUNCT_2:5;
then reconsider T1 = f . x1 as DecoratedTree of IndexedREAL ;
A11: ( dom T1 is finite & T1 is binary ) by A10, Def2;
reconsider T1 = T1 as finite binary DecoratedTree of IndexedREAL by A11, FINSET_1:10;
A12: f . x2 in Initial-Trees p by A6, FUNCT_2:5;
then reconsider T2 = f . x2 as DecoratedTree of IndexedREAL ;
A13: ( dom T2 is finite & T2 is binary ) by A12, Def2;
reconsider T2 = T2 as finite binary DecoratedTree of IndexedREAL by A13, FINSET_1:10;
A14: {} in elementary_tree 0 by TARSKI:def 1, TREES_1:29;
then A15: T1 . {} = [(fcs . x1),(p . {x1})] by A8, FUNCOP_1:7;
A16: fcs . x1 = [(fcs . x1),(p . {x1})] `1
.= [(fcs . x2),(p . {x2})] `1 by A15, A6, A9, A14, FUNCOP_1:7
.= fcs . x2 ;
( x1 in dom fcs & x2 in dom fcs ) by A7, FUNCT_2:def 1;
hence x1 = x2 by A16, FUNCT_1:def 4; :: thesis: verum
end;
then A17: f is one-to-one by FUNCT_1:def 4;
now :: thesis: for z being object st z in Initial-Trees p holds
z in rng f
let z be object ; :: thesis: ( z in Initial-Trees p implies z in rng f )
assume z in Initial-Trees p ; :: thesis: z in rng f
then consider T being Element of FinTrees IndexedREAL such that
A18: ( z = T & T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) ;
consider x being Element of SOURCE such that
A19: T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] by A18;
z = f . x by A19, A18, A5;
hence z in rng f by FUNCT_2:112; :: thesis: verum
end;
then Initial-Trees p c= rng f by TARSKI:def 3;
then A20: Initial-Trees p = rng f by XBOOLE_0:def 10;
dom f = SOURCE by FUNCT_2:def 1;
hence card (Initial-Trees p) = card SOURCE by CARD_1:5, A17, WELLORD2:def 4, A20; :: thesis: verum