for E, F being RealNormSpace
for Q being LinearOperator of E,F
for v being Point of E st Q is one-to-one holds
( Q . v = 0. F iff v = 0. E )