let X, Y be Subset of (bound_QC-variables Al); :: thesis: ( ( for a being object holds
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being object holds
( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) implies X = Y )
assume that
A2: for a being object holds
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) and
A3: for a being object holds
( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ; :: thesis: X = Y
now :: thesis: for a being object holds
( a in X iff a in Y )
let a be object ; :: thesis: ( a in X iff a in Y )
( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) by A2;
hence ( a in X iff a in Y ) by A3; :: thesis: verum
end;
hence X = Y by TARSKI:2; :: thesis: verum