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