let S be non void Signature; :: thesis: for X being ManySortedSet of
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 ; :: 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 });
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 Def2;
consider a being ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 }));
reconsider FX = the Sorts of (Free S,X) as MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) by A2, MSUALG_2:def 10;
FX is opers_closed by A2, MSUALG_2:def 10;
then FX is_closed_on o by MSUALG_2:def 7;
then A3: rng ((Den o,(FreeMSA (X \/ (the carrier of S --> {0 })))) | (((FX # ) * the Arity of S) . o)) c= (FX * the ResultSort of S) . o by MSUALG_2:def 6;
A4: (FX * the ResultSort of S) . o = FX . (the ResultSort of S . o) by FUNCT_2:21
.= FX . (the_result_sort_of o) by MSUALG_1:def 7 ;
A5: 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 9
.= (the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) # ) . (the Arity of S . o) by FUNCT_2:21
.= (the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) # ) . (<*> the carrier of S) by A1, MSUALG_1:def 6
.= {{} } by PRE_CIRC:5 ;
A6: ((FX # ) * the Arity of S) . o = (FX # ) . (the Arity of S . o) by FUNCT_2:21
.= (FX # ) . (<*> the carrier of S) by A1, MSUALG_1:def 6
.= {{} } by PRE_CIRC:5 ;
dom (Den o,(FreeMSA (X \/ (the carrier of S --> {0 })))) c= {{} } by A5;
then A7: (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 A6, RELAT_1:97;
reconsider a = a as Element of Args o,(FreeMSA (X \/ (the carrier of S --> {0 }))) by INSTALG1:2;
a = {} by A5, 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:4;
then root-tree [o,the carrier of S] in rng (Den o,(FreeMSA (X \/ (the carrier of S --> {0 })))) by FUNCT_2:6;
hence root-tree [o,the carrier of S] in the Sorts of (Free S,X) . (the_result_sort_of o) by A3, A4, A7; :: thesis: verum