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))) )
A1: dom ((@ Sub) | (RSub1 (All x,p))) misses dom ((@ Sub) | (RSub2 (All x,p),Sub)) by Th86;
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 A2: 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 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
A3: 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 ) } and
d in rng (@ Sub) and
A4: b = [c,d] by ZFMISC_1:def 2;
A5: ex y1 being bound_QC-variable 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

assume c in RSub2 (All x,p),Sub ; :: thesis: contradiction
then ex y being bound_QC-variable st
( y = c & y in still_not-bound_in (All x,p) & y = (@ Sub) . y ) by Def11;
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:106;
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:96;

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 Def10;
hence contradiction by A5; :: thesis: verum

end;

then not b in [:(RSub1 (All x,p)),(rng (@ Sub)):] by A4, ZFMISC_1:106;
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:96;
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:32;
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 Th86;
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 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) by A10, A11, FUNCT_1:8;
then reconsider z = c as bound_QC-variable ;
A13: d = (@ Sub) . c by A10, A11, FUNCT_1:8;
then A14: d in rng (@ Sub) by A12, FUNCT_1:12;
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:32;
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:96;
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:106;
then A17: z in still_not-bound_in (All x,p) by Def10;
then z in (still_not-bound_in p) \ {x} by QC_LANG3:16;
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:12;
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:96;
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:106;
then ( not z in still_not-bound_in (All x,p) or z <> (@ Sub) . z ) by Def11;
then A20: z <> Sub . z by A16, Def10, SUBSTUT1:def 2;
A21: d in rng (@ Sub) by A12, A13, FUNCT_1:12;
z is Element of dom Sub by A12, SUBSTUT1:def 2;
then 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 ) } by A17, A18, A20;
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 A21, 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;