let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x)
let x be bound_QC-variable of A; :: thesis: for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x)
let p, q be Element of QC-WFF A; :: thesis: (p '&' q) . x = (p . x) '&' (q . x)
set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def 20;
then ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 25, QC_LANG1:def 26;
hence (p '&' q) . x = (p . x) '&' (q . x) by A1, Th20; :: thesis: verum