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