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});
A1: the_arity_of o = {} by Def13;
A2: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) by MSAFREE3:24;
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 A1, MSATERM:24;
A3: variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p) c= MSVars C

proof

let s be object ; :: according to PBOOLE:def 2 :: 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 object ; :: 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:11;
hence x in (MSVars C) . s ; :: thesis: verum

end;

set s9 = the_result_sort_of o;
A4: 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 A2, MSAFREE3:def 5;
then [o, the carrier of C] -tree {} in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A3, A4;
hence [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o by ABCMIZ_1:41; :: thesis: verum