let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution holds @ (RestrictSub x,(All x,p),Sub) = (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)))
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution holds @ (RestrictSub x,(All x,p),Sub) = (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)))
let Sub be CQC_Substitution; :: thesis: @ (RestrictSub x,(All x,p),Sub) = (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)))
set X = { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;
thus @ (RestrictSub x,(All x,p),Sub) c= (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) :: according to XBOOLE_0:def 10 :: thesis: (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) c= @ (RestrictSub x,(All x,p),Sub)

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in @ (RestrictSub x,(All x,p),Sub) or b in (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) )
assume b in @ (RestrictSub x,(All x,p),Sub) ; :: thesis: b in (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)))
then b in RestrictSub x,(All x,p),Sub by SUBSTUT1:def 2;
then b in Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by SUBSTUT1:def 6;
then b in (@ Sub) | { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by SUBSTUT1:def 2;
then b in (@ Sub) /\ [:{ y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ,(rng (@ Sub)):] by RELAT_1:96;
then A1: ( b in @ Sub & b in [:{ y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ,(rng (@ Sub)):] ) by XBOOLE_0:def 4;
then consider c, d being set such that
A2: ( c in { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } & d in rng (@ Sub) & b = [c,d] ) by ZFMISC_1:def 2;
consider y1 being bound_QC-variable such that
A3: ( y1 = c & y1 in still_not-bound_in (All x,p) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) by A2;

A4: now

assume c in RSub1 (All x,p) ; :: thesis: contradiction
then ex y being bound_QC-variable st
( y = c & not y in still_not-bound_in (All x,p) ) by Def11;
hence contradiction by A3; :: thesis: verum

end;

A5: now

assume c in RSub2 (All x,p),Sub ; :: thesis: contradiction
then consider y being bound_QC-variable such that
A6: ( y = c & y in still_not-bound_in (All x,p) & y = (@ Sub) . y ) by Def12;
thus contradiction by A3, A6, SUBSTUT1:def 2; :: thesis: verum

end;

not b in [:(RSub1 (All x,p)),(rng (@ Sub)):] by A2, A4, ZFMISC_1:106;
then not b in (@ Sub) /\ [:(RSub1 (All x,p)),(rng (@ Sub)):] by XBOOLE_0:def 4;
then A7: not b in (@ Sub) | (RSub1 (All x,p)) by RELAT_1:96;
not b in [:(RSub2 (All x,p),Sub),(rng (@ Sub)):] by A2, A5, ZFMISC_1:106;
then not b in (@ Sub) /\ [:(RSub2 (All x,p),Sub),(rng (@ Sub)):] by XBOOLE_0:def 4;
then not b in (@ Sub) | (RSub2 (All x,p),Sub) by RELAT_1:96;
then A8: not b in ((@ Sub) | (RSub1 (All x,p))) \/ ((@ Sub) | (RSub2 (All x,p),Sub)) by A7, XBOOLE_0:def 3;
dom ((@ Sub) | (RSub1 (All x,p))) misses dom ((@ Sub) | (RSub2 (All x,p),Sub)) by Th86;
then not b in ((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)) by A8, FUNCT_4:32;
hence b in (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) by A1, XBOOLE_0:def 5; :: thesis: verum

end;

thus (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) c= @ (RestrictSub x,(All x,p),Sub) :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) or b in @ (RestrictSub x,(All x,p),Sub) )
assume A9: b in (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub))) ; :: thesis: b in @ (RestrictSub x,(All x,p),Sub)
then A10: ( b in @ Sub & not b in ((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)) ) by XBOOLE_0:def 5;
consider c, d being set such that
A11: b = [c,d] by A9, RELAT_1:def 1;
A12: ( c in dom (@ Sub) & d = (@ Sub) . c ) by A10, A11, FUNCT_1:8;
then reconsider z = c as bound_QC-variable ;
dom ((@ Sub) | (RSub1 (All x,p))) misses dom ((@ Sub) | (RSub2 (All x,p),Sub)) by Th86;
then not b in ((@ Sub) | (RSub1 (All x,p))) \/ ((@ Sub) | (RSub2 (All x,p),Sub)) by A10, FUNCT_4:32;
then A13: ( not b in (@ Sub) | (RSub1 (All x,p)) & not b in (@ Sub) | (RSub2 (All x,p),Sub) ) by XBOOLE_0:def 3;
then not b in (@ Sub) /\ [:(RSub1 (All x,p)),(rng (@ Sub)):] by RELAT_1:96;
then A14: not [z,d] in [:(RSub1 (All x,p)),(rng (@ Sub)):] by A10, A11, XBOOLE_0:def 4;
d in rng (@ Sub) by A12, FUNCT_1:12;
then A15: not z in RSub1 (All x,p) by A14, ZFMISC_1:106;
then A16: z in still_not-bound_in (All x,p) by Def11;
then z in (still_not-bound_in p) \ {x} by QC_LANG3:16;
then not z in {x} by XBOOLE_0:def 5;
then A17: z <> x by TARSKI:def 1;
not b in (@ Sub) /\ [:(RSub2 (All x,p),Sub),(rng (@ Sub)):] by A13, RELAT_1:96;
then A18: not [z,d] in [:(RSub2 (All x,p),Sub),(rng (@ Sub)):] by A10, A11, XBOOLE_0:def 4;
d in rng (@ Sub) by A12, FUNCT_1:12;
then not z in RSub2 (All x,p),Sub by A18, ZFMISC_1:106;
then ( not z in still_not-bound_in (All x,p) or z <> (@ Sub) . z ) by Def12;
then A19: z <> Sub . z by A15, Def11, SUBSTUT1:def 2;
z is Element of dom Sub by A12, SUBSTUT1:def 2;
then consider y being bound_QC-variable such that
A20: ( y = z & y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) by A16, A17, A19;
( z in { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } & d in rng (@ Sub) ) by A12, A20, FUNCT_1:12;
then [z,d] in [:{ y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ,(rng (@ Sub)):] by ZFMISC_1:106;
then b in (@ Sub) /\ [:{ y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ,(rng (@ Sub)):] by A10, A11, XBOOLE_0:def 4;
then b in (@ Sub) | { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by RELAT_1:96;
then b in Sub | { y where y is bound_QC-variable : ( y in still_not-bound_in (All x,p) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by SUBSTUT1:def 2;
then b in RestrictSub x,(All x,p),Sub by SUBSTUT1:def 6;
hence b in @ (RestrictSub x,(All x,p),Sub) by SUBSTUT1:def 2; :: thesis: verum

end;