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 A2: 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:9;
variables_in t c= MSVars C by MSAFREE3:28;
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 6;
then A3: e in the Sorts of (Free C,(MSVars C)) . (the_sort_of t) by MSAFREE3:25;
the_sort_of t = the_result_sort_of o by A2, MSATERM:17;
hence e is expression of C, the_result_sort_of o by A3, ABCMIZ_1:def 28; :: thesis: verum