set AL = (((ParsedTerms X) #) * the Arity of S) . o;
set AX = ((ParsedTerms X) * the ResultSort of S) . o;
set D = DTConOSA X;
set O = the carrier' of S;
set rs = the_result_sort_of o;
set RS = the ResultSort of S;
defpred S₁[ object , object ] means for p being FinSequence of TS (DTConOSA X) st p = $1 holds
$2 = (OSSym (o,X)) -tree p;
A1: for x being object st x in (((ParsedTerms X) #) * the Arity of S) . o holds
ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in (((ParsedTerms X) #) * the Arity of S) . o implies ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S₁[x,y] ) )
assume A2: x in (((ParsedTerms X) #) * the Arity of S) . o ; :: thesis: ex y being object st
( y in ((ParsedTerms X) * the ResultSort of S) . o & S₁[x,y] )
then reconsider p = x as FinSequence of TS (DTConOSA X) by Th5;
OSSym (o,X) ==> roots p by A2, Th7;
then reconsider a = (OSSym (o,X)) -tree p as Element of TS (DTConOSA X) by DTCONSTR:def 1;
take y = (OSSym (o,X)) -tree p; :: thesis: ( y in ((ParsedTerms X) * the ResultSort of S) . o & S₁[x,y] )
o in the carrier' of S ;
then o in dom ((ParsedTerms X) * the ResultSort of S) by PARTFUN1:def 2;
then A3: ((ParsedTerms X) * the ResultSort of S) . o = (ParsedTerms X) . ( the ResultSort of S . o) by FUNCT_1:12
.= (ParsedTerms X) . (the_result_sort_of o) by MSUALG_1:def 2
.= ParsedTerms (X,(the_result_sort_of o)) by Def8 ;
a . {} = OSSym (o,X) by TREES_4:def 4;
hence y in ((ParsedTerms X) * the ResultSort of S) . o by A3; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = (((ParsedTerms X) #) * the Arity of S) . o & rng f c= ((ParsedTerms X) * the ResultSort of S) . o & ( for x being object st x in (((ParsedTerms X) #) * the Arity of S) . o holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A1);
reconsider g = f as Function of ((((ParsedTerms X) #) * the Arity of S) . o),(rng f) by A4, FUNCT_2:1;
reconsider g = g as Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) by A4, FUNCT_2:2;
take g ; :: thesis: for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
g . p = (OSSym (o,X)) -tree p
let p be FinSequence of TS (DTConOSA X); :: thesis: ( OSSym (o,X) ==> roots p implies g . p = (OSSym (o,X)) -tree p )
assume OSSym (o,X) ==> roots p ; :: thesis: g . p = (OSSym (o,X)) -tree p
then p in (((ParsedTerms X) #) * the Arity of S) . o by Th7;
hence g . p = (OSSym (o,X)) -tree p by A4; :: thesis: verum