let C be initialized ConstructorSignature; :: thesis: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p is expression of C, the_result_sort_of c
let c be constructor OperSymbol of C; :: thesis: for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p is expression of C, the_result_sort_of c
let p be FinSequence of QuasiTerms C; :: thesis: ( len p = len (the_arity_of c) implies c -trm p is expression of C, the_result_sort_of c )
set X = MSVars C;
set V = (MSVars C) \/ (the carrier of C --> {0 });
assume len p = len (the_arity_of c) ; :: thesis: c -trm p is expression of C, the_result_sort_of c
then A0: (Sym c,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p = c -trm p by TERM;
A1: the Sorts of (Free C,(MSVars C)) = C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:25;
c -trm p is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
then reconsider q = p as ArgumentSeq of Sym c,((MSVars C) \/ (the carrier of C --> {0 })) by A0, MSATERM:1;
rng q c= Union the Sorts of (Free C,(MSVars C)) by FINSEQ_1:def 4;
then c -trm p in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (the_result_sort_of c) by A0, A1, MSAFREE3:20;
hence c -trm p is expression of C, the_result_sort_of c by A1, ELEMENT; :: thesis: verum