let C be initialized ConstructorSignature; :: thesis: for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} holds
ex a being expression of C, an_Adj C st
( a = root-tree [v,the carrier of C] & a is positive )
let m be OperSymbol of C; :: thesis: ( the_result_sort_of m = an_Adj & the_arity_of m = {} implies ex a being expression of C, an_Adj C st
( a = root-tree [m,the carrier of C] & a is positive ) )
assume A2: ( the_result_sort_of m = an_Adj & the_arity_of m = {} ) ; :: thesis: ex a being expression of C, an_Adj C st
( a = root-tree [m,the carrier of C] & a is positive )
set X = MSVars C;
root-tree [m,the carrier of C] in the Sorts of (Free C,(MSVars C)) . an_Adj by A2, MSAFREE3:6;
then reconsider T = root-tree [m,the carrier of C] as expression of C, an_Adj C by Th42;
take T ; :: thesis: ( T = root-tree [m,the carrier of C] & T is positive )
thus T = root-tree [m,the carrier of C] ; :: thesis: T is positive
given a being expression of C, an_Adj C such that A1: T = (non_op C) term a ; :: according to ABCMIZ_1:def 37 :: thesis: contradiction
T = [non_op ,the carrier of C] -tree <*a*> by A1, ThNon;
then [non_op ,the carrier of C] = T . {} by TREES_4:def 4
.= [m,the carrier of C] by TREES_4:3 ;
then m = non_op by ZFMISC_1:33;
hence contradiction by A2, CONSTRSIGN; :: thesis: verum