let l be quasi-loci; :: thesis: for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
set X = rng l;
set n = len l;
set C = MaxConstrSign ;
let s be SortSymbol of MaxConstrSign; :: thesis: for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
let m be constructor OperSymbol of s; :: thesis: ( len (the_arity_of m) = len l implies variables_in (m -trm (args l)) = rng l )
assume A1: len (the_arity_of m) = len l ; :: thesis: variables_in (m -trm (args l)) = rng l
set p = args l;
set Y = { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ;
AA: len (args l) = len (the_arity_of m) by A1, ARGSL;
then A2: variables_in (m -trm (args l)) = union { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } by ABCMIZ_1:90;
B0: dom (args l) = dom l by A1, AA, FINSEQ_3:31;
thus variables_in (m -trm (args l)) c= rng l :: according to XBOOLE_0:def 10 :: thesis: rng l c= variables_in (m -trm (args l))

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in variables_in (m -trm (args l)) or s in rng l )
assume s in variables_in (m -trm (args l)) ; :: thesis: s in rng l
then consider A being set such that
A3: ( s in A & A in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by A2, TARSKI:def 4;
consider t being quasi-term of MaxConstrSign such that
A4: ( A = variables_in t & t in rng (args l) ) by A3;
consider z being set such that
A5: ( z in dom (args l) & t = (args l) . z ) by A4, FUNCT_1:def 5;
reconsider z = z as Element of NAT by A5;
l . z = l /. z by B0, A5, PARTFUN1:def 8;
then A6: l /. z in rng l by B0, A5, FUNCT_1:def 5;
(args l) . z = (l /. z) -term MaxConstrSign by B0, A5, ARGSL;
then A = {(l /. z)} by A4, A5, ABCMIZ_1:86;
hence s in rng l by A3, A6, TARSKI:def 1; :: thesis: verum

end;

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in rng l or s in variables_in (m -trm (args l)) )
assume s in rng l ; :: thesis: s in variables_in (m -trm (args l))
then consider z being set such that
A7: ( z in dom l & s = l . z ) by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A7;
set t = (l /. z) -term MaxConstrSign;
( (args l) . z = (l /. z) -term MaxConstrSign & l . z = l /. z ) by A7, ARGSL, PARTFUN1:def 8;
then ( variables_in ((l /. z) -term MaxConstrSign) = {s} & (l /. z) -term MaxConstrSign in rng (args l) ) by B0, A7, FUNCT_1:def 5, ABCMIZ_1:86;
then ( s in {s} & {s} in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by TARSKI:def 1;
hence s in variables_in (m -trm (args l)) by A2, TARSKI:def 4; :: thesis: verum