let C be initialized ConstructorSignature; :: thesis: for o being nullary OperSymbol of C holds [o,the carrier of C] -tree {} is expression of C, the_result_sort_of o
let o be nullary OperSymbol of C; :: thesis: [o,the carrier of C] -tree {} is expression of C, the_result_sort_of o
set X = MSVars C;
set Z = the carrier of C --> {0 };
set Y = (MSVars C) \/ (the carrier of C --> {0 });
A4: the_arity_of o = {} by Ndef;
B1: the Sorts of (Free C,(MSVars C)) = C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:25;
for i being Nat st i in dom {} holds
ex t being Term of C,((MSVars C) \/ (the carrier of C --> {0 })) st
( t = {} . i & the_sort_of t = (the_arity_of o) . i ) ;
then reconsider p = {} as ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) by A4, MSATERM:24;
A5: variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p) c= MSVars C

proof

let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of C or (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s c= (MSVars C) . s )
assume s in the carrier of C ; :: thesis: (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s c= (MSVars C) . s
then reconsider s9 = s as SortSymbol of C ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s or x in (MSVars C) . s )
assume x in (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s ; :: thesis: x in (MSVars C) . s
then ex t being DecoratedTree st
( t in rng p & x in (C variables_in t) . s9 ) by MSAFREE3:12;
hence x in (MSVars C) . s ; :: thesis: verum

end;

set s9 = the_result_sort_of o;
A7: the_sort_of ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p) = the_result_sort_of o by MSATERM:20;
the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) = { t where t is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C ) } by B1, MSAFREE3:def 6;
then [o,the carrier of C] -tree {} in the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) by A5, A7;
hence [o,the carrier of C] -tree {} is expression of C, the_result_sort_of o by ABCMIZ_1:41; :: thesis: verum