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,()) holds (Den (o,())) . 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,()) holds (Den (o,())) . 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,()) holds (Den (o,())) . x = [o, the carrier of S] -tree x
let x be Element of Args (o,()); :: thesis: (Den (o,())) . x = [o, the carrier of S] -tree x
A1: FreeMSA V = MSAlgebra(# (),() #) 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 () & Sym (o,V) ==> roots p ) by ;
then (DenOp (o,V)) . x = [o, the carrier of S] -tree x by ;
hence (Den (o,())) . x = [o, the carrier of S] -tree x by ; :: thesis: verum