let S be non empty non void ManySortedSign ; for X being ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
let X be ManySortedSet of S; for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
let o be OperSymbol of S; for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
let p be FinSequence; ( p in Args (o,(Free (S,X))) implies (Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p )
assume A1:
p in Args (o,(Free (S,X)))
; (Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
set Y = X (\/) ( the carrier of S --> {0});
consider A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) such that
A2:
( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X )
by MSAFREE3:def 1;
A3:
Free (S,(X (\/) ( the carrier of S --> {0}))) = FreeMSA (X (\/) ( the carrier of S --> {0}))
by MSAFREE3:31;
then
Args (o,(Free (S,X))) c= Args (o,(Free (S,(X (\/) ( the carrier of S --> {0})))))
by A2, MSAFREE3:37;
then
(Den (o,(Free (S,(X (\/) ( the carrier of S --> {0})))))) . p = [o, the carrier of S] -tree p
by A1, A3, INSTALG1:3;
hence
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p
by A1, A2, A3, EQUATION:19; verum