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); :: thesis: ( ( 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 ; :: thesis: f = g

A7: for x being object st x in (((FreeSort X) #) * the Arity of S) . o holds

f . x = g . x

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); :: thesis: ( ( 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 ; :: thesis: f = g

A7: for x being object st x in (((FreeSort X) #) * the Arity of S) . o holds

f . x = g . x

proof

thus
f = g
by A7; :: thesis: verum
let x be object ; :: thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies f . x = g . x )

assume A8: x in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: f . x = g . x

then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;

A9: Sym (o,X) ==> roots p by A8, Th10;

then f . p = (Sym (o,X)) -tree p by A5;

hence f . x = g . x by A6, A9; :: thesis: verum

end;assume A8: x in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: f . x = g . x

then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;

A9: Sym (o,X) ==> roots p by A8, Th10;

then f . p = (Sym (o,X)) -tree p by A5;

hence f . x = g . x by A6, A9; :: thesis: verum