let C be initialized standardized ConstructorSignature; for e being expression of C st (e . {}) `1 in Constructors holds
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
let e be expression of C; ( (e . {}) `1 in Constructors implies ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) )
assume A1:
(e . {}) `1 in Constructors
; ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
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 ) )
;
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )then consider o being
OperSymbol of
C such that A3:
(
e . {} = [o, the carrier of C] & (
o in Constructors or
o = * or
o = non_op ) )
;
take
o
;
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )A4:
(
(e . {}) `1 = o &
(e . {}) `2 = the
carrier of
C )
by A3;
(
* in {*,non_op} &
non_op in {*,non_op} )
by TARSKI:def 2;
then
(
o <> * &
o <> non_op )
by A1, A4, ABCMIZ_1:39, XBOOLE_0:3;
then
o is
constructor
;
hence
(
o = (e . {}) `1 &
the_result_sort_of o = o `1 )
by A3, Def1;
e is expression of C, the_result_sort_of oset X =
MSVars C;
set V =
(MSVars C) (\/) ( the carrier of C --> {0});
reconsider q =
e as
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
A5:
variables_in q c= MSVars C
by MSAFREE3:27;
A6:
the_sort_of q = the_result_sort_of o
by A3, MSATERM:17;
the
Sorts of
(Free (C,(MSVars C))) . (the_result_sort_of o) =
(C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of o)
by MSAFREE3:24
.=
{ a where a is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of a = the_result_sort_of o & variables_in a c= MSVars C ) }
by MSAFREE3:def 5
;
hence
e in the
Sorts of
(Free (C,(MSVars C))) . (the_result_sort_of o)
by A5, A6;
ABCMIZ_1:def 28 verum end; end;