let H be ZF-formula; :: thesis: for E being non empty set st H is universal holds
for f being Function of VAR,E holds
( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St ((the_scope_of H),E) ) ) iff f in St (H,E) )
let E be non empty set ; :: thesis: ( H is universal implies for f being Function of VAR,E holds
( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St ((the_scope_of H),E) ) ) iff f in St (H,E) ) )
assume H is universal ; :: thesis: for f being Function of VAR,E holds
( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St ((the_scope_of H),E) ) ) iff f in St (H,E) )
then H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
hence for f being Function of VAR,E holds
( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St ((the_scope_of H),E) ) ) iff f in St (H,E) ) by Th6; :: thesis: verum