let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let v, vk be SortSymbol of S; :: thesis: for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let o be OperSymbol of S; :: thesis: for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let t be Element of the Sorts of (FreeMSA X) . v; :: thesis: for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let a be ArgumentSeq of Sym (o,X); :: thesis: for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let k be Element of NAT ; :: thesis: for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds
depth ak < depth t
let ak be Element of the Sorts of (FreeMSA X) . vk; :: thesis: ( t = [o, the carrier of S] -tree a & k in dom a & ak = a . k implies depth ak < depth t )
assume that
A1: t = [o, the carrier of S] -tree a and
A2: k in dom a and
A3: ak = a . k ; :: thesis: depth ak < depth t
reconsider a9 = a as DTree-yielding FinSequence ;
A4: ( ex dt being finite DecoratedTree ex tt being finite Tree st
( dt = t & tt = dom dt & depth t = height tt ) & ex q being DTree-yielding FinSequence st
( a9 = q & dom t = tree (doms q) ) ) by A1, MSAFREE2:def 14, TREES_4:def 4;
reconsider da = doms a as FinTree-yielding FinSequence ;
consider dtk being finite DecoratedTree, ttk being finite Tree such that
A5: ( dtk = ak & ttk = dom dtk ) and
A6: depth ak = height ttk by MSAFREE2:def 14;
( dom (doms a9) = dom a9 & ttk = da . k ) by A2, A3, A5, FUNCT_6:22, TREES_3:37;
then ttk in rng da by A2, FUNCT_1:def 3;
hence depth ak < depth t by A6, A4, TREES_3:78; :: thesis: verum