let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))))
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al 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 of Al; :: thesis: for Sub being CQC_Substitution of Al holds @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))))
let Sub be CQC_Substitution of Al; :: 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 of Al : ( 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 object ; :: 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)))) )
A1: dom ((@ Sub) | (RSub1 (All (x,p)))) misses dom ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by Th82;
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 of Al : ( 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 of Al : ( 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 A2: b in (@ Sub) /\ [: { y where y is bound_QC-variable of Al : ( 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:67;
then b in [: { y where y is bound_QC-variable of Al : ( 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 object such that
A3: c in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } and
d in rng (@ Sub) and
A4: b = [c,d] by ZFMISC_1:def 2;
A5: ex y1 being bound_QC-variable of Al st
( y1 = c & y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) by A3;

now :: thesis: not c in RSub2 ((All (x,p)),Sub)

assume c in RSub2 ((All (x,p)),Sub) ; :: thesis: contradiction
then ex y being bound_QC-variable of Al st
( y = c & y in still_not-bound_in (All (x,p)) & y = (@ Sub) . y ) by Def10;
hence contradiction by A5, SUBSTUT1:def 2; :: thesis: verum

end;

then not b in [:(RSub2 ((All (x,p)),Sub)),(rng (@ Sub)):] by A4, ZFMISC_1:87;
then not b in (@ Sub) /\ [:(RSub2 ((All (x,p)),Sub)),(rng (@ Sub)):] by XBOOLE_0:def 4;
then A6: not b in (@ Sub) | (RSub2 ((All (x,p)),Sub)) by RELAT_1:67;

now :: thesis: not c in RSub1 (All (x,p))

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

end;

then not b in [:(RSub1 (All (x,p))),(rng (@ Sub)):] by A4, ZFMISC_1:87;
then not b in (@ Sub) /\ [:(RSub1 (All (x,p))),(rng (@ Sub)):] by XBOOLE_0:def 4;
then not b in (@ Sub) | (RSub1 (All (x,p))) by RELAT_1:67;
then not b in ((@ Sub) | (RSub1 (All (x,p)))) \/ ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by A6, XBOOLE_0:def 3;
then A7: not b in ((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by A1, FUNCT_4:31;
b in @ Sub by A2, XBOOLE_0:def 4;
hence b in (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub)))) by A7, 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

A8: dom ((@ Sub) | (RSub1 (All (x,p)))) misses dom ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by Th82;
let b be object ; :: 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 by XBOOLE_0:def 5;
consider c, d being object such that
A11: b = [c,d] by A9, RELAT_1:def 1;
A12: c in dom (@ Sub) by A10, A11, FUNCT_1:1;
then reconsider z = c as bound_QC-variable of Al ;
A13: d = (@ Sub) . c by A10, A11, FUNCT_1:1;
then A14: d in rng (@ Sub) by A12, FUNCT_1:3;
not b in ((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by A9, XBOOLE_0:def 5;
then A15: not b in ((@ Sub) | (RSub1 (All (x,p)))) \/ ((@ Sub) | (RSub2 ((All (x,p)),Sub))) by A8, FUNCT_4:31;
then not b in (@ Sub) | (RSub1 (All (x,p))) by XBOOLE_0:def 3;
then not b in (@ Sub) /\ [:(RSub1 (All (x,p))),(rng (@ Sub)):] by RELAT_1:67;
then not [z,d] in [:(RSub1 (All (x,p))),(rng (@ Sub)):] by A10, A11, XBOOLE_0:def 4;
then A16: not z in RSub1 (All (x,p)) by A14, ZFMISC_1:87;
then A17: z in still_not-bound_in (All (x,p)) by Def9;
then z in (still_not-bound_in p) \ {x} by QC_LANG3:12;
then not z in {x} by XBOOLE_0:def 5;
then A18: z <> x by TARSKI:def 1;
A19: d in rng (@ Sub) by A12, A13, FUNCT_1:3;
not b in (@ Sub) | (RSub2 ((All (x,p)),Sub)) by A15, XBOOLE_0:def 3;
then not b in (@ Sub) /\ [:(RSub2 ((All (x,p)),Sub)),(rng (@ Sub)):] by RELAT_1:67;
then not [z,d] in [:(RSub2 ((All (x,p)),Sub)),(rng (@ Sub)):] by A10, A11, XBOOLE_0:def 4;
then not z in RSub2 ((All (x,p)),Sub) by A19, ZFMISC_1:87;
then ( not z in still_not-bound_in (All (x,p)) or z <> (@ Sub) . z ) by Def10;
then A20: z <> Sub . z by A16, Def9, SUBSTUT1:def 2;
A21: d in rng (@ Sub) by A12, A13, FUNCT_1:3;
z is Element of dom Sub by A12, SUBSTUT1:def 2;
then z in { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A17, A18, A20;
then [z,d] in [: { y where y is bound_QC-variable of Al : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ,(rng (@ Sub)):] by A21, ZFMISC_1:87;
then b in (@ Sub) /\ [: { y where y is bound_QC-variable of Al : ( 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 of Al : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by RELAT_1:67;
then b in Sub | { y where y is bound_QC-variable of Al : ( 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;