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) } ;
A2: len (args l) = len (the_arity_of m) by A1, Def18;
then A3: 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;
A4: dom (args l) = dom l by A1, A2, FINSEQ_3:29;
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 object ; :: 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
A5: ( s in A & A in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by A3, TARSKI:def 4;
consider t being quasi-term of MaxConstrSign such that
A6: ( A = variables_in t & t in rng (args l) ) by A5;
consider z being object such that
A7: ( z in dom (args l) & t = (args l) . z ) by A6, FUNCT_1:def 3;
reconsider z = z as Element of NAT by A7;
l . z = l /. z by A4, A7, PARTFUN1:def 6;
then A8: l /. z in rng l by A4, A7, FUNCT_1:def 3;
(args l) . z = (l /. z) -term MaxConstrSign by A4, A7, Def18;
then A = {(l /. z)} by A6, A7, ABCMIZ_1:86;
hence s in rng l by A5, A8, TARSKI:def 1; :: thesis: verum

end;

let s be object ; :: 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 object such that
A9: ( z in dom l & s = l . z ) by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A9;
set t = (l /. z) -term MaxConstrSign;
( (args l) . z = (l /. z) -term MaxConstrSign & l . z = l /. z ) by A9, Def18, PARTFUN1:def 6;
then ( variables_in ((l /. z) -term MaxConstrSign) = {s} & (l /. z) -term MaxConstrSign in rng (args l) ) by A4, A9, ABCMIZ_1:86, FUNCT_1:def 3;
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 A3, TARSKI:def 4; :: thesis: verum