let C be initialized standardized ConstructorSignature; :: thesis: 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; :: thesis: ( (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 ; :: thesis: 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 Th49;

suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) ; :: thesis: 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 x being Element of Vars such that
A2: ( e = x -term C & e . {} = [x,a_Term ] ) ;
( (e . {} ) `1 = x & x in Vars ) by A2, MCART_1:7;
hence 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 ) by A1, XBOOLE_0:3, Lem2; :: 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: 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
A2: ( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ;
take o ; :: thesis: ( o = (e . {} ) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
A3: ( (e . {} ) `1 = o & (e . {} ) `2 = the carrier of C ) by A2, MCART_1:7;
( * in {* ,non_op } & non_op in {* ,non_op } ) by TARSKI:def 2;
then ( o <> * & o <> non_op ) by A1, A3, XBOOLE_0:3, ABCMIZ_1:39;
then o is constructor by ABCMIZ_1:def 11;
hence ( o = (e . {} ) `1 & the_result_sort_of o = o `1 ) by A2, MCART_1:7, StandardizedDef; :: thesis: e is expression of C, the_result_sort_of o
set 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:9;
A4: variables_in q c= MSVars C by MSAFREE3:28;
A5: the_sort_of q = the_result_sort_of o by A2, 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:25
.= { 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 6 ;
hence e in the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) by A4, A5; :: according to ABCMIZ_1:def 28 :: thesis: verum

end;

end;