set AL = ((() #) * the Arity of S) . o;
set AX = (() * the ResultSort of S) . o;
set D = DTConMSA X;
let f, g be Function of (((() #) * the Arity of S) . o),((() * the ResultSort of S) . o); :: thesis: ( ( for p being FinSequence of TS () st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS () st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p ) implies f = g )

assume that
A5: for p being FinSequence of TS () st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p and
A6: for p being FinSequence of TS () st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p ; :: thesis: f = g
A7: for x being object st x in ((() #) * the Arity of S) . o holds
f . x = g . x
proof
let x be object ; :: thesis: ( x in ((() #) * the Arity of S) . o implies f . x = g . x )
assume A8: x in ((() #) * the Arity of S) . o ; :: thesis: f . x = g . x
then reconsider p = x as FinSequence of TS () by Th8;
A9: Sym (o,X) ==> roots p by ;
then f . p = (Sym (o,X)) -tree p by A5;
hence f . x = g . x by A6, A9; :: thesis: verum
end;
thus f = g by A7; :: thesis: verum