let C be initialized ConstructorSignature; :: thesis: for e being expression of C
for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
let e be expression of C; :: thesis: for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
let o be OperSymbol of C; :: thesis: ( e . {} = [o, the carrier of C] implies e is expression of C, the_result_sort_of o )
assume A1: e . {} = [o, the carrier of C] ; :: thesis: e is expression of C, the_result_sort_of o
set X = MSVars C;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
variables_in t c= MSVars C by MSAFREE3:27;
then e in { t1 where t1 is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ;
then e in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def 5;
then A2: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24;
the_sort_of t = the_result_sort_of o by A1, MSATERM:17;
hence e is expression of C, the_result_sort_of o by A2, ABCMIZ_1:def 28; :: thesis: verum