let x, y be bound_QC-variable; :: thesis: for p being Element of QC-WFF st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let p be Element of QC-WFF ; :: 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 19;
then ( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x ) by QC_LANG1:def 25, QC_LANG1:def 26;
hence ( x <> y implies (All (x,p)) . y = All (x,(p . y)) ) by A1, Th36; :: thesis: verum