let X be finite Subset of Vars; :: thesis: ( varcl X = X implies for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X ) )
assume A1: varcl X = X ; :: thesis: for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
then consider l being quasi-loci such that
A2: rng l = X by Th31;
set n = len l;
set C = MaxConstrSign ;
let s be SortSymbol of MaxConstrSign; :: thesis: ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
consider m being constructor OperSymbol of s such that
A3: len (the_arity_of m) = len l by Th57;
take m ; :: thesis: ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
set p = args l;
take args l ; :: thesis: ( len (args l) = len (the_arity_of m) & vars (m -trm (args l)) = X )
thus len (args l) = len (the_arity_of m) by A3, Def18; :: thesis: vars (m -trm (args l)) = X
thus vars (m -trm (args l)) = X by A1, A2, A3, Th58; :: thesis: verum