set AL = (((FreeSort X) #) * the Arity of S) . o;
set AX = ((FreeSort X) * the ResultSort of S) . o;
set D = DTConMSA X;
let f, g be Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o); ( ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) 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 (DTConMSA X) st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p
and
A6:
for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p
; f = g
A7:
for x being object st x in (((FreeSort X) #) * the Arity of S) . o holds
f . x = g . x
thus
f = g
by A7; verum