:: deftheorem defuker defines UKer DUALSP04:def 13 :
for X being RealUnitarySpace
for f being linear-Functional of X
for b₃ being strict Subspace of X holds
( b₃ = UKer f iff the carrier of b₃ = f " {0} );