let C be initialized ConstructorSignature; :: thesis: for c being constructor OperSymbol of C
for e being expression of C
for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }
let c be constructor OperSymbol of C; :: thesis: for e being expression of C
for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }
let e be expression of C; :: thesis: for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }
let p be DTree-yielding FinSequence; :: thesis: ( e = [c, the carrier of C] -tree p implies variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p } )
set X = { (variables_in t) where t is quasi-term of C : t in rng p } ;
assume A1: e = [c, the carrier of C] -tree p ; :: thesis: variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }
then p in (QuasiTerms C) * by Th51;
then p is FinSequence of QuasiTerms C by FINSEQ_1:def 11;
then A2: rng p c= QuasiTerms C by FINSEQ_1:def 4;
thus variables_in e c= union { (variables_in t) where t is quasi-term of C : t in rng p } :: according to XBOOLE_0:def 10 :: thesis: union { (variables_in t) where t is quasi-term of C : t in rng p } c= variables_in e
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in e or a in union { (variables_in t) where t is quasi-term of C : t in rng p } )
assume a in variables_in e ; :: thesis: a in union { (variables_in t) where t is quasi-term of C : t in rng p }
then consider t being DecoratedTree such that
A3: t in rng p and
A4: a in (C variables_in t) . (a_Term C) by A1, MSAFREE3:11;
reconsider t = t as quasi-term of C by A2, A3, Th41;
variables_in t in { (variables_in t) where t is quasi-term of C : t in rng p } by A3;
hence a in union { (variables_in t) where t is quasi-term of C : t in rng p } by A4, TARSKI:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (variables_in t) where t is quasi-term of C : t in rng p } or a in variables_in e )
assume a in union { (variables_in t) where t is quasi-term of C : t in rng p } ; :: thesis: a in variables_in e
then consider Y being set such that
A5: a in Y and
A6: Y in { (variables_in t) where t is quasi-term of C : t in rng p } by TARSKI:def 4;
ex t being quasi-term of C st
( Y = variables_in t & t in rng p ) by A6;
hence a in variables_in e by A1, A5, MSAFREE3:11; :: thesis: verum