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 holds
p . x = IFEQ ((bound_in p),x,p,(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 holds
p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x))))
let p be Element of QC-WFF A; :: thesis: ( p is universal implies p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) )
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: p . x = F . p and
A2: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) by Def3;
consider G being Function of (QC-WFF A),(QC-WFF A) such that
A3: (the_scope_of p) . x = G . (the_scope_of p) and
A4: for q being Element of QC-WFF A holds
( G . (VERUM A) = VERUM A & ( q is atomic implies G . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies G . q = 'not' (G . (the_argument_of q)) ) & ( q is conjunctive implies G . q = (G . (the_left_argument_of q)) '&' (G . (the_right_argument_of q)) ) & ( q is universal implies G . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(G . (the_scope_of q))))) ) ) by Def3;
F = G by A2, A4, Lm2;
hence ( p is universal implies p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) ) by A1, A2, A3; :: thesis: verum