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 Z0: 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
A0: rng l = X by ThLoci;
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
A1: len (the_arity_of m) = len l by Th61;
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 )
set Y = { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ;
thus len (args l) = len (the_arity_of m) by A1, ARGSL; :: thesis: vars (m -trm (args l)) = X
thus vars (m -trm (args l)) = X by Z0, A0, A1, Th63; :: thesis: verum