set A = DTConUA (f,D);
set i = f /. n;
set Y = (dom f) \/ D;
set smm = Sym (n,f,D);
defpred S₁[ object , object ] means ( $1 in (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p = $1 holds
$2 = (Sym (n,f,D)) -tree p ) );
set tu = { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } ;
A2: f /. n = f . n by A1, PARTFUN1:def 6;
A3: for x, y being object st x in (TS (DTConUA (f,D))) * & S₁[x,y] holds
y in TS (DTConUA (f,D))

proof

reconsider sm = Sym (n,f,D) as Element of (dom f) \/ D ;
let x, y be object ; :: thesis: ( x in (TS (DTConUA (f,D))) * & S₁[x,y] implies y in TS (DTConUA (f,D)) )
assume that
x in (TS (DTConUA (f,D))) * and
A4: S₁[x,y] ; :: thesis: y in TS (DTConUA (f,D))
consider s being Element of (TS (DTConUA (f,D))) * such that
A5: s = x and
A6: len s = f /. n by A4;
A7: y = (Sym (n,f,D)) -tree s by A4, A5;
reconsider s = s as FinSequence of TS (DTConUA (f,D)) ;
( dom (roots s) = dom s & Seg (len (roots s)) = dom (roots s) ) by FINSEQ_1:def 3, TREES_3:def 18;
then A8: len (roots s) = f /. n by A6, FINSEQ_1:def 3;
reconsider s = s as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ;
reconsider rs = roots s as Element of ((dom f) \/ D) * by FINSEQ_1:def 11;
sm = n by A1, Def9;
then [sm,rs] in REL (f,D) by A1, A2, A8, Def7;
then Sym (n,f,D) ==> roots s by LANG1:def 1;
hence y in TS (DTConUA (f,D)) by A7, DTCONSTR:def 1; :: thesis: verum

end;

A9: for x, y1, y2 being object st x in (TS (DTConUA (f,D))) * & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( x in (TS (DTConUA (f,D))) * & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
x in (TS (DTConUA (f,D))) * and
A10: S₁[x,y1] and
A11: S₁[x,y2] ; :: thesis: y1 = y2
consider s being Element of (TS (DTConUA (f,D))) * such that
A12: s = x and
len s = f /. n by A10;
y1 = (Sym (n,f,D)) -tree s by A10, A12;
hence y1 = y2 by A11, A12; :: thesis: verum

end;

consider F being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) such that
A13: for x being object holds
( x in dom F iff ( x in (TS (DTConUA (f,D))) * & ex y being object st S₁[x,y] ) ) and
A14: for x being object st x in dom F holds
S₁[x,F . x] from PARTFUN1:sch 2(A3, A9);
A15: dom F = (f /. n) -tuples_on (TS (DTConUA (f,D)))

proof

thus dom F c= (f /. n) -tuples_on (TS (DTConUA (f,D))) :: according to XBOOLE_0:def 10 :: thesis: (f /. n) -tuples_on (TS (DTConUA (f,D))) c= dom F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in (f /. n) -tuples_on (TS (DTConUA (f,D))) )
assume x in dom F ; :: thesis: x in (f /. n) -tuples_on (TS (DTConUA (f,D)))
then ex y being object st S₁[x,y] by A13;
hence x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; :: thesis: verum

end;

reconsider sm = Sym (n,f,D) as Symbol of (DTConUA (f,D)) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f /. n) -tuples_on (TS (DTConUA (f,D))) or x in dom F )
assume x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; :: thesis: x in dom F
then consider s being Element of (TS (DTConUA (f,D))) * such that
A16: s = x and
A17: len s = f /. n ;
S₁[s,sm -tree s] by A17;
hence x in dom F by A13, A16; :: thesis: verum

end;

A18: for x, y being FinSequence of TS (DTConUA (f,D)) st len x = len y & x in dom F holds
y in dom F

proof

let x, y be FinSequence of TS (DTConUA (f,D)); :: thesis: ( len x = len y & x in dom F implies y in dom F )
assume that
A19: len x = len y and
A20: x in dom F ; :: thesis: y in dom F
reconsider sy = y as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def 11;
ex sx being Element of (TS (DTConUA (f,D))) * st
( sx = x & len sx = f /. n ) by A15, A20;
then sy in { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } by A19;
hence y in dom F by A15; :: thesis: verum

end;

A21: ex x being FinSequence st x in dom F

proof

set a = the Element of (f /. n) -tuples_on (TS (DTConUA (f,D)));
the Element of (f /. n) -tuples_on (TS (DTConUA (f,D))) in dom F by A15;
hence ex x being FinSequence st x in dom F ; :: thesis: verum

end;

dom F is with_common_domain

proof

let x, y be FinSequence; :: according to MARGREL1:def 1 :: thesis: ( not x in dom F or not y in dom F or len x = len y )
assume ( x in dom F & y in dom F ) ; :: thesis: len x = len y
then ( ex sx being Element of (TS (DTConUA (f,D))) * st
( sx = x & len sx = f /. n ) & ex sy being Element of (TS (DTConUA (f,D))) * st
( sy = y & len sy = f /. n ) ) by A15;
hence len x = len y ; :: thesis: verum

end;

then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) by A18, A21, MARGREL1:def 21, MARGREL1:def 22;
take F ; :: thesis: ( dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds
F . p = (Sym (n,f,D)) -tree p ) )
thus dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) by A15; :: thesis: for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds
F . p = (Sym (n,f,D)) -tree p
let p be FinSequence of TS (DTConUA (f,D)); :: thesis: ( p in dom F implies F . p = (Sym (n,f,D)) -tree p )
assume p in dom F ; :: thesis: F . p = (Sym (n,f,D)) -tree p
hence F . p = (Sym (n,f,D)) -tree p by A14; :: thesis: verum