set A = FreeGen (s,X);
set D = DTConMSA X;
defpred S₁[ 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₁[x,a] )

proof

let x be object ; :: thesis: ( x in FreeGen (s,X) implies ex a being object st
( a in X . s & S₁[x,a] ) )
assume x in FreeGen (s,X) ; :: thesis: ex a being object 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 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₁[x,a] )
thus a in X . s by A4, A5, A6; :: 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; :: 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
S₁[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