set FG = FreeGen X;
set D = DTConMSA X;
consider s being SortSymbol of S, x being set such that
x in X . s and
A2: t = [x,s] by A1, Th7;
(FreeGen X) . s = FreeGen (s,X) by Def16;
then A3: dom (F . s) = FreeGen (s,X) by FUNCT_2:def 1
.= { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by Th13 ;
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 ( rng (F . s) c= A . s & A . s in rng A ) by FUNCT_1:def 3, RELAT_1:def 19;
then (F . s) . (root-tree t) in union (rng A) by A4, 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