set A = FreeGen s,X;
set D = DTConMSA X;
defpred S₁[ set , set ] means for t being Symbol of (DTConMSA X) st $1 = root-tree t holds
$2 = t `1 ;
A1: for x being set st x in FreeGen s,X holds
ex a being set st
( a in X . s & S₁[x,a] )

proof

let x be set ; :: thesis: ( x in FreeGen s,X implies ex a being set st
( a in X . s & S₁[x,a] ) )
assume x in FreeGen s,X ; :: thesis: ex a being set st
( a in X . s & S₁[x,a] )
then x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by Th14;
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₁[x,a] )
thus a in X . s by A4, A5, A6, MCART_1:7; :: thesis: S₁[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, MCART_1:7; :: thesis: verum

end;

consider f being Function such that
A7: ( dom f = FreeGen s,X & rng f c= X . s & ( for x being set st x in FreeGen s,X holds
S₁[x,f . x] ) ) from WELLORD2:sch 1(A1);
reconsider f = f as Function of (FreeGen s,X),(X . s) by A7, FUNCT_2:4;
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