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

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