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 Th11;
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;
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, Th8, XBOOLE_0:3; :: 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
A3: ( 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 )
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; :: 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: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; :: according to ABCMIZ_1:def 28 :: thesis: verum
end;
end;