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
main-constr (c -trm p) = 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
main-constr (c -trm p) = c
let p be FinSequence of QuasiTerms C; :: thesis: ( len p = len (the_arity_of c) implies main-constr (c -trm p) = c )
assume len p = len (the_arity_of c) ; :: thesis: main-constr (c -trm p) = c
then c -trm p = [c, the carrier of C] -tree p by ABCMIZ_1:def 35;
then (c -trm p) . {} = [c, the carrier of C] by TREES_4:def 4;
hence main-constr (c -trm p) = [c, the carrier of C] `1 by Def9
.= c ;
:: thesis: verum