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 A1: (Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p = c -trm p by Def35;
A2: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) by MSAFREE3:24;
c -trm p is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
then reconsider q = p as ArgumentSeq of Sym (c,((MSVars C) (\/) ( the carrier of C --> {0}))) by A1, 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 A1, A2, MSAFREE3:19;
hence c -trm p is expression of C, the_result_sort_of c by A2, Def28; :: thesis: verum