set A = FreeGen (s,X);
set D = DTConMSA X;
defpred S1[ object , object ] means for t being Symbol of () 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 & S1[x,a] )
proof
let x be object ; :: thesis: ( x in FreeGen (s,X) implies ex a being object st
( a in X . s & S1[x,a] ) )

assume x in FreeGen (s,X) ; :: thesis: ex a being object st
( a in X . s & S1[x,a] )

then x in { () where t is Symbol of () : ( t in Terminals () & t `2 = s ) } by Th13;
then consider t being Symbol of () such that
A2: x = root-tree t and
A3: t in Terminals () 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 ;
take a ; :: thesis: ( a in X . s & S1[x,a] )
thus a in X . s by A4, A5, A6; :: thesis: S1[x,a]
let t1 be Symbol of (); :: thesis: ( x = root-tree t1 implies a = t1 `1 )
assume x = root-tree t1 ; :: thesis: a = t1 `1
then t = t1 by ;
hence a = t1 `1 by A6; :: thesis: verum
end;
consider f being Function such that
A7: ( dom f = FreeGen (s,X) & rng f c= X . s & ( for x being object st x in FreeGen (s,X) holds
S1[x,f . x] ) ) from reconsider f = f as Function of (FreeGen (s,X)),(X . s) by ;
take f ; :: thesis: for t being Symbol of () st root-tree t in FreeGen (s,X) holds
f . () = t `1

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