let C be initialized standardized ConstructorSignature; 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; ( ( (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
o being
OperSymbol of
C st
(
e . {} = [o, the carrier of C] & (
o in Constructors or
o = * or
o = non_op ) )
;
( ( (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;
verum end;