let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for V being V16() 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 V16() 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 V16() 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 16;
reconsider p = x as ArgumentSeq of Sym o,V by Th2;
A2: Sym o,V = [o,the carrier of S] by MSAFREE:def 11;
( 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 14;
hence (Den o,(FreeMSA V)) . x = [o,the carrier of S] -tree x by A1, MSAFREE:def 15; :: thesis: verum