set A = FreeGen (s,X);

set D = DTConMSA X;

defpred S_{1}[ object , object ] means for t being Symbol of (DTConMSA X) st $1 = root-tree t holds

$2 = t `1 ;

A1: for x being object st x in FreeGen (s,X) holds

ex a being object st

( a in X . s & S_{1}[x,a] )

A7: ( dom f = FreeGen (s,X) & rng f c= X . s & ( for x being object st x in FreeGen (s,X) holds

S_{1}[x,f . x] ) )
from FUNCT_1:sch 6(A1);

reconsider f = f as Function of (FreeGen (s,X)),(X . s) by A7, FUNCT_2:2;

take f ; :: thesis: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

f . (root-tree t) = t `1

let t be Symbol of (DTConMSA X); :: thesis: ( root-tree t in FreeGen (s,X) implies f . (root-tree t) = t `1 )

assume root-tree t in FreeGen (s,X) ; :: thesis: f . (root-tree t) = t `1

hence f . (root-tree t) = t `1 by A7; :: thesis: verum

set D = DTConMSA X;

defpred S

$2 = t `1 ;

A1: for x being object st x in FreeGen (s,X) holds

ex a being object st

( a in X . s & S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in FreeGen (s,X) implies ex a being object st

( a in X . s & S_{1}[x,a] ) )

assume x in FreeGen (s,X) ; :: thesis: ex a being object st

( a in X . s & S_{1}[x,a] )

then x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by Th13;

then consider t being Symbol of (DTConMSA X) such that

A2: x = root-tree t and

A3: t in Terminals (DTConMSA X) and

A4: t `2 = s ;

consider s1 being SortSymbol of S, a being set such that

A5: a in X . s1 and

A6: t = [a,s1] by A3, Th7;

take a ; :: thesis: ( a in X . s & S_{1}[x,a] )

thus a in X . s by A4, A5, A6; :: thesis: S_{1}[x,a]

let t1 be Symbol of (DTConMSA X); :: thesis: ( x = root-tree t1 implies a = t1 `1 )

assume x = root-tree t1 ; :: thesis: a = t1 `1

then t = t1 by A2, TREES_4:4;

hence a = t1 `1 by A6; :: thesis: verum

end;( a in X . s & S

assume x in FreeGen (s,X) ; :: thesis: ex a being object st

( a in X . s & S

then x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by Th13;

then consider t being Symbol of (DTConMSA X) such that

A2: x = root-tree t and

A3: t in Terminals (DTConMSA X) and

A4: t `2 = s ;

consider s1 being SortSymbol of S, a being set such that

A5: a in X . s1 and

A6: t = [a,s1] by A3, Th7;

take a ; :: thesis: ( a in X . s & S

thus a in X . s by A4, A5, A6; :: thesis: S

let t1 be Symbol of (DTConMSA X); :: thesis: ( x = root-tree t1 implies a = t1 `1 )

assume x = root-tree t1 ; :: thesis: a = t1 `1

then t = t1 by A2, TREES_4:4;

hence a = t1 `1 by A6; :: thesis: verum

A7: ( dom f = FreeGen (s,X) & rng f c= X . s & ( for x being object st x in FreeGen (s,X) holds

S

reconsider f = f as Function of (FreeGen (s,X)),(X . s) by A7, FUNCT_2:2;

take f ; :: thesis: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds

f . (root-tree t) = t `1

let t be Symbol of (DTConMSA X); :: thesis: ( root-tree t in FreeGen (s,X) implies f . (root-tree t) = t `1 )

assume root-tree t in FreeGen (s,X) ; :: thesis: f . (root-tree t) = t `1

hence f . (root-tree t) = t `1 by A7; :: thesis: verum