let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let v be Element of Valuations_in (Al,A); :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let xSQ be second_Q_comp of [S,x]; :: thesis: for a being Element of A st [S,x] is quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
let a be Element of A; :: thesis: ( [S,x] is quantifiable implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) )
set S1 = CQCSub_All ([S,x],xSQ);
set z = S_Bound (@ (CQCSub_All ([S,x],xSQ)));
set finSub = RestrictSub (x,(All (x,(S `1))),xSQ);
set V1 = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a));
set V2 = v . ((NEx_Val (v,S,x,xSQ)) +* (x | a));
set X = still_not-bound_in (S `1);
A1: dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) = (dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) \/ (dom ((NEx_Val (v,S,x,xSQ)) +* (x | a))) by FUNCT_4:def 1;
dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) = bound_QC-variables Al by Th58;
then dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) = dom v by Th58;
then A2: dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) = dom (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) by A1, FUNCT_4:def 1;
assume A3: [S,x] is quantifiable ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
A4: now :: thesis: ( not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) )
assume not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
then A5: S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x by A3, Th52;
for b being object st b in dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
proof
let b be object ; :: thesis: ( b in dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b )
assume A6: b in dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
A7: now :: thesis: ( b <> S_Bound (@ (CQCSub_All ([S,x],xSQ))) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b )
assume A8: b <> S_Bound (@ (CQCSub_All ([S,x],xSQ))) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
A9: now :: thesis: ( not b in dom (NEx_Val (v,S,x,xSQ)) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b )
A10: not b in dom (x | a) by A5, A8, TARSKI:def 1;
assume not b in dom (NEx_Val (v,S,x,xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
then not b in (dom (NEx_Val (v,S,x,xSQ))) \/ (dom (x | a)) by A10, XBOOLE_0:def 3;
then A11: not b in dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)) by FUNCT_4:def 1;
reconsider x = b as bound_QC-variable of Al by A6;
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . b by A11, FUNCT_4:11;
then ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = v . x by A8, Th48;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b by A11, FUNCT_4:11; :: thesis: verum
end;
now :: thesis: ( b in dom (NEx_Val (v,S,x,xSQ)) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b )
dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)) = (dom (NEx_Val (v,S,x,xSQ))) \/ (dom (x | a)) by FUNCT_4:def 1;
then A12: dom (NEx_Val (v,S,x,xSQ)) c= dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)) by XBOOLE_1:7;
assume A13: b in dom (NEx_Val (v,S,x,xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
then ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = ((NEx_Val (v,S,x,xSQ)) +* (x | a)) . b by A12, FUNCT_4:13;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b by A13, A12, FUNCT_4:13; :: thesis: verum
end;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b by A9; :: thesis: verum
end;
now :: thesis: ( b = S_Bound (@ (CQCSub_All ([S,x],xSQ))) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b )
assume b = S_Bound (@ (CQCSub_All ([S,x],xSQ))) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b
then b in {x} by A5, TARSKI:def 1;
then A14: b in dom (x | a) ;
dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)) = (dom (NEx_Val (v,S,x,xSQ))) \/ (dom (x | a)) by FUNCT_4:def 1;
then A15: dom (x | a) c= dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)) by XBOOLE_1:7;
then ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = ((NEx_Val (v,S,x,xSQ)) +* (x | a)) . b by A14, FUNCT_4:13;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b by A14, A15, FUNCT_4:13; :: thesis: verum
end;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) . b by A7; :: thesis: verum
end;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) by A2, FUNCT_1:2; :: thesis: verum
end;
now :: thesis: ( x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) )
assume A16: x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
A17: dom (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) = ((dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) \/ (dom ((NEx_Val (v,S,x,xSQ)) +* (x | a)))) /\ (still_not-bound_in (S `1)) by A1, RELAT_1:61;
A18: for b being object st b in dom (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) holds
(((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b
proof
A19: still_not-bound_in (S `1) c= Bound_Vars (S `1) by Th47;
let b be object ; :: thesis: ( b in dom (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) implies (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b )
assume A20: b in dom (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b
b in still_not-bound_in (S `1) by A17, A20, XBOOLE_0:def 4;
then A21: b <> S_Bound (@ (CQCSub_All ([S,x],xSQ))) by A3, A16, A19, Th38;
A22: (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v | (still_not-bound_in (S `1))) +* (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) by FUNCT_4:71;
A23: ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) | (still_not-bound_in (S `1))) +* (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) by FUNCT_4:71;
then A24: dom (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) = (dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) | (still_not-bound_in (S `1)))) \/ (dom (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1)))) by FUNCT_4:def 1;
A25: now :: thesis: ( not b in dom (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) implies (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b )
assume A26: not b in dom (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b
then A27: b in dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) | (still_not-bound_in (S `1))) by A20, A24, XBOOLE_0:def 3;
then b in (dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a))) /\ (still_not-bound_in (S `1)) by RELAT_1:61;
then A28: b in still_not-bound_in (S `1) by XBOOLE_0:def 4;
b in bound_QC-variables Al by A20;
then b in dom v by Th58;
then A29: b in (dom v) /\ (still_not-bound_in (S `1)) by A28, XBOOLE_0:def 4;
(((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) | (still_not-bound_in (S `1))) . b by A23, A26, FUNCT_4:11;
then (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . b by A27, FUNCT_1:47;
then A30: (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = v . b by A21, Th48;
((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = (v | (still_not-bound_in (S `1))) . b by A22, A26, FUNCT_4:11;
hence (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b by A30, A29, FUNCT_1:48; :: thesis: verum
end;
now :: thesis: ( b in dom (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) implies (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b )
assume A31: b in dom (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) ; :: thesis: (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b
then (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = (((NEx_Val (v,S,x,xSQ)) +* (x | a)) | (still_not-bound_in (S `1))) . b by A23, FUNCT_4:13;
hence (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b by A22, A31, FUNCT_4:13; :: thesis: verum
end;
hence (((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b = ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) . b by A25; :: thesis: verum
end;
dom ((v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))) = (dom ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)))) /\ (still_not-bound_in (S `1)) by A2, RELAT_1:61;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) by A18, FUNCT_1:2, RELAT_1:61; :: thesis: verum
end;
hence ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) by A4; :: thesis: verum