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 = All ((bound_in p),((the_scope_of p) . x))
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 = All ((bound_in p),((the_scope_of p) . x))
let p be Element of QC-WFF A; :: thesis: ( p is universal & bound_in p <> x implies p . x = All ((bound_in p),((the_scope_of p) . x)) )
assume p is universal ; :: thesis: ( not bound_in p <> x or p . x = All ((bound_in p),((the_scope_of p) . x)) )
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 = All ((bound_in p),((the_scope_of p) . x)) ) by FUNCOP_1:def 8; :: thesis: verum