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))); ( 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
; f1 = f2
now for x being object st x in (f /. n) -tuples_on (TS (DTConUA (f,D))) holds
f1 . x = f2 . xlet x be
object ;
( 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)))
;
f1 . x = f2 . xthen 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;
verum end;
hence
f1 = f2
by A22, A24, FUNCT_1:2; verum