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 20;
then ( the_scope_of (All x,p) = p & bound_in (All x,p) = x ) by QC_LANG1:def 26, QC_LANG1:def 27;
hence ( x <> y implies (All x,p) . y = All x,(p . y) ) by A1, Th36; :: thesis: verum