let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for V being V5() ManySortedSet of
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 V5() ManySortedSet of
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 V5() ManySortedSet of ; :: 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
reconsider p = x as ArgumentSeq of Sym o,V by Th2;
( p is FinSequence of TS (DTConMSA V) & Sym o,V ==> roots p & Sym o,V = [o,the carrier of S] ) by MSAFREE:def 11, MSATERM:21, MSATERM:def 1;
then ( (DenOp o,V) . x = [o,the carrier of S] -tree x & (FreeOper V) . o = DenOp o,V & FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) ) by MSAFREE:def 14, MSAFREE:def 15, MSAFREE:def 16;
hence (Den o,(FreeMSA V)) . x = [o,the carrier of S] -tree x ; :: thesis: verum