let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C holds
( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
let e be expression of C; :: thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )

per cases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;

suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) ; :: thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )

then consider x being Element of Vars such that
A1: ( e = x -term C & e . {} = [x,a_Term] ) ;
thus ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A1; :: thesis: verum

end;

suppose ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; :: thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )

then consider o being OperSymbol of C such that
A2: e . {} = [o, the carrier of C] ;
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 A3: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24;
A4: ( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38;
A5: ( (e . {}) `1 = o & non_op C = non_op & ast C = * ) by A2;
the_sort_of t = the_result_sort_of o by A2, MSATERM:17;
hence ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A3, A4, A5, ABCMIZ_1:def 28; :: thesis: verum

end;

end;