let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for V being non-empty ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let o be OperSymbol of S; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let x be Element of Args (o,(FreeMSA V)); :: thesis: (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
A1: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def 14;
reconsider p = x as ArgumentSeq of Sym (o,V) by Th1;
A2: Sym (o,V) = [o, the carrier of S] by MSAFREE:def 9;
( p is FinSequence of TS (DTConMSA V) & Sym (o,V) ==> roots p ) by MSATERM:21, MSATERM:def 1;
then (DenOp (o,V)) . x = [o, the carrier of S] -tree x by A2, MSAFREE:def 12;
hence (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x by A1, MSAFREE:def 13; :: thesis: verum