let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal & bound_in p = x holds
p . x = p
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st p is universal & bound_in p = x holds
p . x = p
let p be Element of QC-WFF A; :: thesis: ( p is universal & bound_in p = x implies p . x = p )
assume p is universal ; :: thesis: ( not bound_in p = x or p . x = p )
then p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) by Lm3;
hence ( not bound_in p = x or p . x = p ) by FUNCOP_1:def 8; :: thesis: verum