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
variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }
let c be constructor OperSymbol of C; :: thesis: for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }
let p be FinSequence of QuasiTerms C; :: thesis: ( len p = len (the_arity_of c) implies variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p } )
assume len p = len (the_arity_of c) ; :: thesis: variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }
then c -trm p = [c, the carrier of C] -tree p by Def35;
hence variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p } by Th88; :: thesis: verum