let l be quasi-loci; 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; 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; ( 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
; 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
XBOOLE_0:def 10 rng l c= variables_in (m -trm (args l))proof
let s be
object ;
TARSKI:def 3 ( not s in variables_in (m -trm (args l)) or s in rng l )
assume
s in variables_in (m -trm (args l))
;
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;
verum
end;
let s be object ; TARSKI:def 3 ( not s in rng l or s in variables_in (m -trm (args l)) )
assume
s in rng l
; 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; verum