let A be QC-alphabet ; :: thesis: for x, y being bound_QC-variable of A
for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let x, y be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let p be Element of QC-WFF A; :: thesis: ( x <> y implies (All (x,p)) . y = All (x,(p . y)) )
set q = All (x,p);
A1: All (x,p) is universal by QC_LANG1:def 21;
then ( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x ) by QC_LANG1:def 27, QC_LANG1:def 28;
hence ( x <> y implies (All (x,p)) . y = All (x,(p . y)) ) by A1, Th23; :: thesis: verum