set A = TS (DTConUA (f,D));
let f1, f2 be non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); :: thesis: ( dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds
f1 . p = (Sym (n,f,D)) -tree p ) & dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds
f2 . p = (Sym (n,f,D)) -tree p ) implies f1 = f2 )
assume that
A22: dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and
A23: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds
f1 . p = (Sym (n,f,D)) -tree p and
A24: dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and
A25: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds
f2 . p = (Sym (n,f,D)) -tree p ; :: thesis: f1 = f2

now :: thesis: for x being object st x in (f /. n) -tuples_on (TS (DTConUA (f,D))) holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in (f /. n) -tuples_on (TS (DTConUA (f,D))) implies f1 . x = f2 . x )
assume A26: x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; :: thesis: f1 . x = f2 . x
then consider s being Element of (TS (DTConUA (f,D))) * such that
A27: s = x and
len s = f /. n ;
f1 . s = (Sym (n,f,D)) -tree s by A22, A23, A26, A27;
hence f1 . x = f2 . x by A24, A25, A26, A27; :: thesis: verum

end;

hence f1 = f2 by A22, A24, FUNCT_1:2; :: thesis: verum