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
vars e = union { (vars 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
vars e = union { (vars 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
vars e = union { (vars 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 vars e = union { (vars t) where t is quasi-term of C : t in rng p } )
assume A1: e = [c, the carrier of C] -tree p ; :: thesis: vars e = union { (vars t) where t is quasi-term of C : t in rng p }
set A = { (variables_in t) where t is quasi-term of C : t in rng p } ;
set B = { (vars t) where t is quasi-term of C : t in rng p } ;

per cases ( { (variables_in t) where t is quasi-term of C : t in rng p } = {} or { (variables_in t) where t is quasi-term of C : t in rng p } <> {} ) ;

suppose A2: { (variables_in t) where t is quasi-term of C : t in rng p } = {} ; :: thesis: vars e = union { (vars t) where t is quasi-term of C : t in rng p }

set b = the Element of { (vars t) where t is quasi-term of C : t in rng p } ;

now :: thesis: not { (vars t) where t is quasi-term of C : t in rng p } <> {}

assume { (vars t) where t is quasi-term of C : t in rng p } <> {} ; :: thesis: contradiction
then the Element of { (vars t) where t is quasi-term of C : t in rng p } in { (vars t) where t is quasi-term of C : t in rng p } ;
then consider t being quasi-term of C such that
the Element of { (vars t) where t is quasi-term of C : t in rng p } = vars t and
A3: t in rng p ;
variables_in t in { (variables_in t) where t is quasi-term of C : t in rng p } by A3;
hence contradiction by A2; :: thesis: verum

end;

hence vars e = union { (vars t) where t is quasi-term of C : t in rng p } by A1, A2, Th8, Th88, ZFMISC_1:2; :: thesis: verum

end;

suppose { (variables_in t) where t is quasi-term of C : t in rng p } <> {} ; :: thesis: vars e = union { (vars t) where t is quasi-term of C : t in rng p }

then reconsider A = { (variables_in t) where t is quasi-term of C : t in rng p } as non empty set ;
set D = { (varcl s) where s is Element of A : verum } ;
A4: { (vars t) where t is quasi-term of C : t in rng p } c= { (varcl s) where s is Element of A : verum }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (vars t) where t is quasi-term of C : t in rng p } or a in { (varcl s) where s is Element of A : verum } )
assume a in { (vars t) where t is quasi-term of C : t in rng p } ; :: thesis: a in { (varcl s) where s is Element of A : verum }
then consider t being quasi-term of C such that
A5: a = vars t and
A6: t in rng p ;
variables_in t in A by A6;
then reconsider s = variables_in t as Element of A ;
a = varcl s by A5;
hence a in { (varcl s) where s is Element of A : verum } ; :: thesis: verum

end;

A7: { (varcl s) where s is Element of A : verum } c= { (vars t) where t is quasi-term of C : t in rng p }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (varcl s) where s is Element of A : verum } or a in { (vars t) where t is quasi-term of C : t in rng p } )
assume a in { (varcl s) where s is Element of A : verum } ; :: thesis: a in { (vars t) where t is quasi-term of C : t in rng p }
then consider s being Element of A such that
A8: a = varcl s ;
s in A ;
then consider t being quasi-term of C such that
A9: s = variables_in t and
A10: t in rng p ;
vars t = a by A8, A9;
hence a in { (vars t) where t is quasi-term of C : t in rng p } by A10; :: thesis: verum

end;

thus vars e = varcl (union A) by A1, Th88
.= union { (varcl s) where s is Element of A : verum } by Th10
.= union { (vars t) where t is quasi-term of C : t in rng p } by A4, A7, XBOOLE_0:def 10 ; :: thesis: verum

end;

end;