let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S

for V being V2() 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 V2() 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 V2() 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

for V being V2() 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 V2() 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 V2() 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