let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st p is atomic holds
p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((a. 0) .--> x)))
let p be Element of QC-WFF ; :: thesis: ( p is atomic implies p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((a. 0) .--> x))) )
ex F being Function of QC-WFF,QC-WFF st
( p . x = F . p & ( for q being Element of QC-WFF holds
( F . VERUM = VERUM & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((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 Def6;
hence ( p is atomic implies p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((a. 0) .--> x))) ) ; :: thesis: verum