let C be initialized ConstructorSignature; :: thesis: for c being constructor OperSymbol of C
for a being expression of C, an_Adj C
for t being expression of C, a_Type C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)
let c be constructor OperSymbol of C; :: thesis: for a being expression of C, an_Adj C
for t being expression of C, a_Type C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)
let a be expression of C, an_Adj C; :: thesis: for t being expression of C, a_Type C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)
let t be expression of C, a_Type C; :: thesis: for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)
let p be FinSequence of QuasiTerms C; :: thesis: ( len p = len (the_arity_of c) implies c -trm p <> (ast C) term (a,t) )
assume len p = len (the_arity_of c) ; :: thesis: c -trm p <> (ast C) term (a,t)
then c -trm p = [c, the carrier of C] -tree p by Def35;
then A1: (c -trm p) . {} = [c, the carrier of C] by TREES_4:def 4;
assume c -trm p = (ast C) term (a,t) ; :: thesis: contradiction
then c -trm p = [*, the carrier of C] -tree <*a,t*> by Th46;
then [c, the carrier of C] = [*, the carrier of C] by A1, TREES_4:def 4;
then c = * by XTUPLE_0:1;
hence contradiction by Def11; :: thesis: verum