let p be ZF-formula; :: thesis: for x being Variable holds
( bound_in (All x,p) = x & the_scope_of (All x,p) = p )
let x be Variable; :: thesis: ( bound_in (All x,p) = x & the_scope_of (All x,p) = p )
All x,p is universal by ZF_LANG:16;
then All x,p = All (bound_in (All x,p)),(the_scope_of (All x,p)) by ZF_LANG:62;
hence ( bound_in (All x,p) = x & the_scope_of (All x,p) = p ) by ZF_LANG:12; :: thesis: verum