let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds
for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
let X be V5() ManySortedSet of the carrier of S; for o being OperSymbol of S
for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds
for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
let o be OperSymbol of S; for p being DTree-yielding FinSequence st [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) holds
for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
let p be DTree-yielding FinSequence; ( [o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) implies for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )
A1:
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #)
by MSAFREE:def 14;
assume A2:
[o, the carrier of S] -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o)
; for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
now for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
the
carrier of
S in { the carrier of S}
by TARSKI:def 1;
then
[o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:]
by ZFMISC_1:87;
then reconsider nt =
[o, the carrier of S] as
NonTerminal of
(DTConMSA X) by MSAFREE:6;
set rso =
the_result_sort_of o;
reconsider ao =
the_arity_of o as
Element of the
carrier of
S * ;
let i be
Nat;
( i in dom (the_arity_of o) implies p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) )assume A3:
i in dom (the_arity_of o)
;
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)then
ao . i in rng ao
by FUNCT_1:def 3;
then reconsider s =
ao . i as
SortSymbol of
S ;
A4: the
Sorts of
(FreeMSA X) . s =
FreeSort (
X,
s)
by A1, MSAFREE:def 11
.=
FreeSort (
X,
((the_arity_of o) /. i))
by A3, PARTFUN1:def 6
;
[o, the carrier of S] -tree p in FreeSort (
X,
(the_result_sort_of o))
by A2, A1, MSAFREE:def 11;
then
[o, the carrier of S] -tree p in { a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . (the_result_sort_of o) & a = root-tree [x,(the_result_sort_of o)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = the_result_sort_of o ) ) }
by MSAFREE:def 10;
then consider a being
Element of
TS (DTConMSA X) such that A5:
a = [o, the carrier of S] -tree p
and
( ex
x being
set st
(
x in X . (the_result_sort_of o) &
a = root-tree [x,(the_result_sort_of o)] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a . {} &
the_result_sort_of o = the_result_sort_of o ) )
;
a . {} = [o, the carrier of S]
by A5, TREES_4:def 4;
then consider ts being
FinSequence of
TS (DTConMSA X) such that A6:
a = nt -tree ts
and A7:
nt ==> roots ts
by DTCONSTR:10;
nt = Sym (
o,
X)
by MSAFREE:def 9;
then A8:
ts in (((FreeSort X) #) * the Arity of S) . o
by A7, MSAFREE:10;
(
dom p = Seg (len p) &
dom (the_arity_of o) = Seg (len (the_arity_of o)) )
by FINSEQ_1:def 3;
then A9:
i in dom p
by A2, A3, Th10;
reconsider ts =
ts as
DTree-yielding FinSequence ;
ts = p
by A5, A6, TREES_4:15;
hence
p . i in the
Sorts of
(FreeMSA X) . ((the_arity_of o) . i)
by A9, A8, A4, MSAFREE:9;
verum end;
hence
for i being Nat st i in dom (the_arity_of o) holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i)
; verum