set AL = (((ParsedTerms X) # ) * the Arity of S) . o;
set AX = ((ParsedTerms X) * the ResultSort of S) . o;
set D = DTConOSA X;
let f, g be Function of ((((ParsedTerms X) # ) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o); :: thesis: ( ( for p being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots p holds
f . p = (OSSym o,X) -tree p ) & ( for p being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots p holds
g . p = (OSSym o,X) -tree p ) implies f = g )
assume that
A6: for p being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots p holds
f . p = (OSSym o,X) -tree p and
A7: for p being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots p holds
g . p = (OSSym o,X) -tree p ; :: thesis: f = g
A8: ( dom f = (((ParsedTerms X) # ) * the Arity of S) . o & dom g = (((ParsedTerms X) # ) * the Arity of S) . o ) by FUNCT_2:def 1;
for x being set st x in (((ParsedTerms X) # ) * the Arity of S) . o holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in (((ParsedTerms X) # ) * the Arity of S) . o implies f . x = g . x )
assume A9: x in (((ParsedTerms X) # ) * the Arity of S) . o ; :: thesis: f . x = g . x
then reconsider p = x as FinSequence of TS (DTConOSA X) by Th5;
OSSym o,X ==> roots p by A9, Th7;
then ( f . p = (OSSym o,X) -tree p & g . p = (OSSym o,X) -tree p ) by A6, A7;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A8, FUNCT_1:9; :: thesis: verum