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

proof

for a being set holds
( a in { y where y is bound_QC-variable : ( 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 : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } )

proof

let a be set ; :: thesis: ( a in { y where y is bound_QC-variable : ( 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 : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } )
thus ( a in { y where y is bound_QC-variable : ( 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 : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis: ( a in Z /\ { y where y is bound_QC-variable : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable : ( 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 : ( 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 : ( y is Element of dom Sub & y <> x & y <> Sub . y ) }
then consider y being bound_QC-variable such that
A1: ( a = y & y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) ;
( y in still_not-bound_in p & y in { y where y is bound_QC-variable : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) by A1;
hence a in Z /\ { y where y is bound_QC-variable : ( 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 : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) :: thesis: verum

proof

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

end;

end;

hence { y where y is bound_QC-variable : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } = Z /\ { y where y is bound_QC-variable : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by TARSKI:2; :: thesis: verum

end;

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