let SOURCE be non empty finite set ; for p being Probability of Trivial-SigmaField SOURCE holds union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let p be Probability of Trivial-SigmaField SOURCE; union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
set L = union (LeavesSet (Initial-Trees p));
set R = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } ;
reconsider fcs = (canFS SOURCE) " as Function of SOURCE,(Seg (card SOURCE)) by FINSEQ_1:95;
for x being object holds
( x in union (LeavesSet (Initial-Trees p)) iff x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
proof
let x be
object ;
( x in union (LeavesSet (Initial-Trees p)) iff x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
hereby ( x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } implies x in union (LeavesSet (Initial-Trees p)) )
assume
x in union (LeavesSet (Initial-Trees p))
;
x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } then consider Y being
set such that A1:
(
x in Y &
Y in LeavesSet (Initial-Trees p) )
by TARSKI:def 4;
consider q being
Element of
BinFinTrees IndexedREAL such that A2:
(
Y = Leaves q &
q in Initial-Trees p )
by A1;
consider T being
Element of
FinTrees IndexedREAL such that A3:
(
q = T &
T is
finite binary DecoratedTree of
IndexedREAL & ex
y being
Element of
SOURCE st
T = root-tree [(((canFS SOURCE) ") . y),(p . {y})] )
by A2;
reconsider T =
T as
finite binary DecoratedTree of
IndexedREAL by A3;
consider y being
Element of
SOURCE such that A4:
T = root-tree [(((canFS SOURCE) ") . y),(p . {y})]
by A3;
Y = {[(((canFS SOURCE) ") . y),(p . {y})]}
by A2, A3, A4, Th16;
then
x = [(((canFS SOURCE) ") . y),(p . {y})]
by TARSKI:def 1, A1;
hence
x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
by A1;
verum
end;
assume
x in { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
;
x in union (LeavesSet (Initial-Trees p))
then consider z being
Element of
[:NAT,REAL:] such that A5:
(
x = z & ex
y being
Element of
SOURCE st
z = [(((canFS SOURCE) ") . y),(p . {y})] )
;
consider y being
Element of
SOURCE such that A6:
z = [(((canFS SOURCE) ") . y),(p . {y})]
by A5;
fcs . y in NAT
by TARSKI:def 3;
then A7:
[(fcs . y),(p . {y})] in [:NAT,REAL:]
by ZFMISC_1:87;
set T =
root-tree [(fcs . y),(p . {y})];
A8:
dom (root-tree [(fcs . y),(p . {y})]) = elementary_tree 0
;
then
root-tree [(fcs . y),(p . {y})] is
Element of
FinTrees IndexedREAL
by TREES_3:def 8, A7;
then A9:
root-tree [(fcs . y),(p . {y})] in Initial-Trees p
;
reconsider T =
root-tree [(fcs . y),(p . {y})] as
Element of
BinFinTrees IndexedREAL by A7, A8, Def2;
Leaves T = {[(((canFS SOURCE) ") . y),(p . {y})]}
by Th16;
then A10:
x in Leaves T
by TARSKI:def 1, A5, A6;
Leaves T in LeavesSet (Initial-Trees p)
by A9;
hence
x in union (LeavesSet (Initial-Trees p))
by TARSKI:def 4, A10;
verum
end;
hence
union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
by TARSKI:2; verum