let SOURCE be non empty finite set ; for p being Probability of Trivial-SigmaField SOURCE holds card (Initial-Trees p) = card SOURCE
let p be Probability of Trivial-SigmaField SOURCE; 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 ;
( x in SOURCE implies ex y being object st
( y in Initial-Trees p & S2[x,y] ) )
assume A2:
x in SOURCE
;
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})];
( 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;
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 for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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 )
;
x1 = x2then 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;
verum end;
then A17:
f is one-to-one
by FUNCT_1:def 4;
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; verum