reconsider fcs = (canFS SOURCE) " as Function of SOURCE,(Seg (card SOURCE)) by FINSEQ_1:95;
set S = { 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})] ) } ;

now :: thesis: for z being object st z in { 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})] ) } holds
z in BinFinTrees IndexedREAL

let z be object ; :: thesis: ( z in { 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})] ) } implies z in BinFinTrees IndexedREAL )
assume z in { 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})] ) } ; :: thesis: z in BinFinTrees IndexedREAL
then ex T being Element of FinTrees IndexedREAL st
( z = T & T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) ;
then reconsider z0 = z as finite binary DecoratedTree of IndexedREAL ;
( dom z0 is finite & dom z0 is binary ) by BINTREE1:def 3;
hence z in BinFinTrees IndexedREAL by Def2; :: thesis: verum

end;

then reconsider S = { 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})] ) } as Subset of (BinFinTrees IndexedREAL) by TARSKI:def 3;
consider x being object such that
A1: x in SOURCE by XBOOLE_0:def 1;
reconsider x = x as Element of SOURCE by A1;
A2: fcs . x in NAT by TARSKI:def 3;
A3: [(fcs . x),(p . {x})] in [:NAT,REAL:] by A2, ZFMISC_1:87;
set T = root-tree [(fcs . x),(p . {x})];
dom (root-tree [(fcs . x),(p . {x})]) = elementary_tree 0 ;
then root-tree [(fcs . x),(p . {x})] is Element of FinTrees IndexedREAL by A3, TREES_3:def 8;
then A4: root-tree [(fcs . x),(p . {x})] in S ;
for z being object st z in S holds
z in Funcs ((elementary_tree 0),[:(Seg (card SOURCE)),(rng p):])

proof

let z be object ; :: thesis: ( z in S implies z in Funcs ((elementary_tree 0),[:(Seg (card SOURCE)),(rng p):]) )
assume z in S ; :: thesis: z in Funcs ((elementary_tree 0),[:(Seg (card SOURCE)),(rng p):])
then consider T being Element of FinTrees IndexedREAL such that
A5: ( z = T & T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(fcs . x),(p . {x})] ) ;
consider x being Element of SOURCE such that
A6: T = root-tree [(fcs . x),(p . {x})] by A5;
A7: dom T = elementary_tree 0 by A5;
A8: rng T = {[(fcs . x),(p . {x})]} by A6, FUNCOP_1:8;
{x} in bool SOURCE ;
then {x} in dom p by FUNCT_2:def 1;
then p . {x} in rng p by FUNCT_1:3;
then rng T c= [:(Seg (card SOURCE)),(rng p):] by A8, ZFMISC_1:31, ZFMISC_1:87;
hence z in Funcs ((elementary_tree 0),[:(Seg (card SOURCE)),(rng p):]) by A5, A7, FUNCT_2:def 2; :: thesis: verum

end;

then S c= Funcs ((elementary_tree 0),[:(Seg (card SOURCE)),(rng p):]) by TARSKI:def 3;
hence { 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})] ) } is non empty finite Subset of (BinFinTrees IndexedREAL) by A4; :: thesis: verum