let C be initialized ConstructorSignature; :: thesis: for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
let q be pure expression of C, a_Type C; :: thesis: for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
let A be finite Subset of (QuasiAdjs C); :: thesis: vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)
set X = { (variables_in a) where a is quasi-adjective of C : a in A } ;
set Y = { (vars a) where a is quasi-adjective of C : a in A } ;
A1: union { (variables_in a) where a is quasi-adjective of C : a in A } c= union { (vars a) where a is quasi-adjective of C : a in A }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (variables_in a) where a is quasi-adjective of C : a in A } or x in union { (vars a) where a is quasi-adjective of C : a in A } )
assume x in union { (variables_in a) where a is quasi-adjective of C : a in A } ; :: thesis: x in union { (vars a) where a is quasi-adjective of C : a in A }
then consider Z being set such that
A2: x in Z and
A3: Z in { (variables_in a) where a is quasi-adjective of C : a in A } by TARSKI:def 4;
consider a being quasi-adjective of C such that
A4: Z = variables_in a and
A5: a in A by A3;
A6: Z c= vars a by A4, Def1;
vars a in { (vars a) where a is quasi-adjective of C : a in A } by A5;
hence x in union { (vars a) where a is quasi-adjective of C : a in A } by A2, A6, TARSKI:def 4; :: thesis: verum
end;
for x, y being set st [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } holds
x c= union { (vars a) where a is quasi-adjective of C : a in A }
proof
let x, y be set ; :: thesis: ( [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } implies x c= union { (vars a) where a is quasi-adjective of C : a in A } )
assume [x,y] in union { (vars a) where a is quasi-adjective of C : a in A } ; :: thesis: x c= union { (vars a) where a is quasi-adjective of C : a in A }
then consider Z being set such that
A7: [x,y] in Z and
A8: Z in { (vars a) where a is quasi-adjective of C : a in A } by TARSKI:def 4;
ex a being quasi-adjective of C st
( Z = vars a & a in A ) by A8;
then A9: x c= Z by A7, Def1;
Z c= union { (vars a) where a is quasi-adjective of C : a in A } by A8, ZFMISC_1:74;
hence x c= union { (vars a) where a is quasi-adjective of C : a in A } by A9; :: thesis: verum
end;
then A10: varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) c= union { (vars a) where a is quasi-adjective of C : a in A } by A1, Def1;
A11: union { (vars a) where a is quasi-adjective of C : a in A } c= varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (vars a) where a is quasi-adjective of C : a in A } or x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) )
assume x in union { (vars a) where a is quasi-adjective of C : a in A } ; :: thesis: x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )
then consider Z being set such that
A12: x in Z and
A13: Z in { (vars a) where a is quasi-adjective of C : a in A } by TARSKI:def 4;
consider a being quasi-adjective of C such that
A14: Z = vars a and
A15: a in A by A13;
variables_in a in { (variables_in a) where a is quasi-adjective of C : a in A } by A15;
then vars a c= varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) by Th9, ZFMISC_1:74;
hence x in varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } ) by A12, A14; :: thesis: verum
end;
thus vars (A ast q) = varcl ((union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)) by Th104
.= (varcl (union { (variables_in a) where a is quasi-adjective of C : a in A } )) \/ (vars q) by Th11
.= (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q) by A10, A11, XBOOLE_0:def 10 ; :: thesis: verum