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
A21: dom f1 = (f /. n) -tuples_on (TS (DTConUA f,D)) and
A22: for p being FinSequence of TS (DTConUA f,D) st p in dom f1 holds
f1 . p = (Sym n,f,D) -tree p and
A23: dom f2 = (f /. n) -tuples_on (TS (DTConUA f,D)) and
A24: 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

let x be set ; :: thesis: ( x in (f /. n) -tuples_on (TS (DTConUA f,D)) implies f1 . x = f2 . x )
assume A25: 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
A26: s = x and
len s = f /. n ;
f1 . s = (Sym n,f,D) -tree s by A21, A22, A25, A26;
hence f1 . x = f2 . x by A23, A24, A25, A26; :: thesis: verum

end;

hence f1 = f2 by A21, A23, FUNCT_1:9; :: thesis: verum