set FG = PTVars X;
set D = DTConOSA X;
consider s being Element of S, x being set such that
x in X . s and
A2: t = [x,s] by A1, Th4;
(PTVars X) . s = PTVars (s,X) by Def24;
then A3: dom (F . s) = PTVars (s,X) by FUNCT_2:def 1
.= { (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) } by Th28 ;
t `2 = s by A2;
then root-tree t in dom (F . s) by A1, A3;
then A4: (F . s) . (root-tree t) in rng (F . s) by FUNCT_1:def 3;
dom A = the carrier of S by PARTFUN1:def 2;
then A5: A . s in rng A by FUNCT_1:def 3;
rng (F . s) c= A . s by RELAT_1:def 19;
then (F . s) . (root-tree t) in union (rng A) by A4, A5, TARSKI:def 4;
then reconsider eu = (F . s) . (root-tree t) as Element of Union A by CARD_3:def 4;
take eu ; :: thesis: for f being Function st f = F . (t `2) holds
eu = f . (root-tree t)
let f be Function; :: thesis: ( f = F . (t `2) implies eu = f . (root-tree t) )
assume f = F . (t `2) ; :: thesis: eu = f . (root-tree t)
hence eu = f . (root-tree t) by A2; :: thesis: verum