let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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))) ; :: thesis: (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; :: thesis: verum