set A = DTConUA (f,D);
set i = f /. n;
set Y = (dom f) \/ D;
set smm = Sym (n,f,D);
defpred S1[ 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))) * & S1[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 ;
( x in (TS (DTConUA (f,D))) * & S1[x,y] implies y in TS (DTConUA (f,D)) )
assume that
x in (TS (DTConUA (f,D))) *
and A4:
S1[
x,
y]
;
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;
verum
end;
A9:
for x, y1, y2 being object st x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that
x in (TS (DTConUA (f,D))) *
and A10:
S1[
x,
y1]
and A11:
S1[
x,
y2]
;
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;
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 S1[x,y] ) )
and
A14:
for x being object st x in dom F holds
S1[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)))
XBOOLE_0:def 10 (f /. n) -tuples_on (TS (DTConUA (f,D))) c= dom F
reconsider sm =
Sym (
n,
f,
D) as
Symbol of
(DTConUA (f,D)) ;
let x be
object ;
TARSKI:def 3 ( 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)))
;
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
;
S1[
s,
sm -tree s]
by A17;
hence
x in dom F
by A13, A16;
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
A21:
ex x being FinSequence st x in dom F
dom F is with_common_domain
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
; ( 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; 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)); ( p in dom F implies F . p = (Sym (n,f,D)) -tree p )
assume
p in dom F
; F . p = (Sym (n,f,D)) -tree p
hence
F . p = (Sym (n,f,D)) -tree p
by A14; verum