let x be bound_QC-variable; :: thesis: for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
let v be Element of Valuations_in A; :: thesis: for S being Element of CQC-Sub-WFF st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
let S be Element of CQC-Sub-WFF ; :: thesis: ( x in dom (S `2) implies v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x )
assume x in dom (S `2) ; :: thesis: v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
then ( (v . (Val_S (v,S))) . x = (Val_S (v,S)) . x & x in dom (@ (S `2)) ) by Th13, SUBSTUT1:def 2;
hence v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x by FUNCT_1:13; :: thesis: verum