let C be initialized ConstructorSignature; 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; 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; ( 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)
; 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; verum