let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S

for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

let X be ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) )

assume A1: the_arity_of o = {} ; :: thesis: root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

set Y = X (\/) ( the carrier of S --> {0});

A2: Args (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) = (( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) * the Arity of S) . o by MSUALG_1:def 4

.= ( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) . ( the Arity of S . o) by FUNCT_2:15

.= ( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) . (<*> the carrier of S) by A1, MSUALG_1:def 1

.= {{}} by PRE_CIRC:2 ;

then A3: dom (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) c= {{}} ;

A4: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then reconsider FX = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

((FX #) * the Arity of S) . o = (FX #) . ( the Arity of S . o) by FUNCT_2:15

.= (FX #) . (<*> the carrier of S) by A1, MSUALG_1:def 1

.= {{}} by PRE_CIRC:2 ;

then A5: (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o) = Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) by A3, RELAT_1:68;

set a = the ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0})));

reconsider a = the ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) as Element of Args (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) by INSTALG1:1;

a = {} by A2, TARSKI:def 1;

then root-tree [o, the carrier of S] = [o, the carrier of S] -tree a by TREES_4:20;

then (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) . a = root-tree [o, the carrier of S] by INSTALG1:3;

then A6: root-tree [o, the carrier of S] in rng (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) by FUNCT_2:4;

FX is opers_closed by A4, MSUALG_2:def 9;

then FX is_closed_on o ;

then A7: rng ((Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o)) c= (FX * the ResultSort of S) . o ;

(FX * the ResultSort of S) . o = FX . ( the ResultSort of S . o) by FUNCT_2:15

.= FX . (the_result_sort_of o) by MSUALG_1:def 2 ;

hence root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) by A7, A5, A6; :: thesis: verum

for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

let X be ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) )

assume A1: the_arity_of o = {} ; :: thesis: root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

set Y = X (\/) ( the carrier of S --> {0});

A2: Args (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) = (( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) * the Arity of S) . o by MSUALG_1:def 4

.= ( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) . ( the Arity of S . o) by FUNCT_2:15

.= ( the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) #) . (<*> the carrier of S) by A1, MSUALG_1:def 1

.= {{}} by PRE_CIRC:2 ;

then A3: dom (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) c= {{}} ;

A4: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then reconsider FX = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

((FX #) * the Arity of S) . o = (FX #) . ( the Arity of S . o) by FUNCT_2:15

.= (FX #) . (<*> the carrier of S) by A1, MSUALG_1:def 1

.= {{}} by PRE_CIRC:2 ;

then A5: (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o) = Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) by A3, RELAT_1:68;

set a = the ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0})));

reconsider a = the ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) as Element of Args (o,(FreeMSA (X (\/) ( the carrier of S --> {0})))) by INSTALG1:1;

a = {} by A2, TARSKI:def 1;

then root-tree [o, the carrier of S] = [o, the carrier of S] -tree a by TREES_4:20;

then (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) . a = root-tree [o, the carrier of S] by INSTALG1:3;

then A6: root-tree [o, the carrier of S] in rng (Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) by FUNCT_2:4;

FX is opers_closed by A4, MSUALG_2:def 9;

then FX is_closed_on o ;

then A7: rng ((Den (o,(FreeMSA (X (\/) ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o)) c= (FX * the ResultSort of S) . o ;

(FX * the ResultSort of S) . o = FX . ( the ResultSort of S . o) by FUNCT_2:15

.= FX . (the_result_sort_of o) by MSUALG_1:def 2 ;

hence root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) by A7, A5, A6; :: thesis: verum