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 st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
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 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 (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x
let v be Element of Valuations_in (Al,A); :: thesis: for S being Element of CQC-Sub-WFF Al 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 Al; :: 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 Th12, SUBSTUT1:def 2;
hence v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x by FUNCT_1:13; :: thesis: verum