set FG = FreeGen X;
set D = DTConMSA X;
consider s being SortSymbol of S, x being set such that
A2: ( x in X . s & t = [x,s] ) by A1, Th7;
(FreeGen X) . s = FreeGen s,X by Def18;
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 Th14 ;
t `2 = s by A2, MCART_1:7;
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 5;
A5: rng (F . s) c= A . s by RELAT_1:def 19;
dom A = the carrier of S by PARTFUN1:def 4;
then A . s in rng A by FUNCT_1:def 5;
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, MCART_1:7; :: thesis: verum