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 that
A1: the_result_sort_of m = an_Adj and
A2: 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 A1, A2, MSAFREE3:5;
then reconsider T = root-tree [m, the carrier of C] as expression of C, an_Adj C by Th41;
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 A3: T = (non_op C) term a ; :: according to ABCMIZ_1:def 37 :: thesis: contradiction
T = [non_op, the carrier of C] -tree <*a*> by A3, Th43;
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 XTUPLE_0:1;
hence contradiction by A2, Def9; :: thesis: verum