set Y = { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
set X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
reconsider Z = still_not-bound_in p as finite set by CQC_SIM1:19;
for a being object holds
( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } iff a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } )

proof

let a be object ; :: thesis: ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } iff a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } )
thus ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis: ( a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } )

proof

assume a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; :: thesis: a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) }
then consider y being bound_QC-variable of A such that
A1: ( a = y & y in still_not-bound_in p ) and
A2: ( y is Element of dom Sub & y <> x & y <> Sub . y ) ;
y in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A2;
hence a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A1, XBOOLE_0:def 4; :: thesis: verum

end;

thus ( a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis: verum

proof

assume A3: a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ; :: thesis: a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) }
then a in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by XBOOLE_0:def 4;
then A4: ex y being bound_QC-variable of A st
( a = y & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
a in Z by A3, XBOOLE_0:def 4;
hence a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4; :: thesis: verum

end;

end;

then reconsider X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } as finite set by TARSKI:2;
Sub | X is finite ;
hence Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A ; :: thesis: verum