let E, F be RealNormSpace; :: thesis: 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 )
let Q be LinearOperator of E,F; :: thesis: for v being Point of E st Q is one-to-one holds
( Q . v = 0. F iff v = 0. E )
let v be Point of E; :: thesis: ( Q is one-to-one implies ( Q . v = 0. F iff v = 0. E ) )
assume A1: Q is one-to-one ; :: thesis: ( Q . v = 0. F iff v = 0. E )
hereby :: thesis: ( v = 0. E implies Q . v = 0. F )
assume A2: Q . v = 0. F ; :: thesis: v = 0. E
A3: dom Q = the carrier of E by FUNCT_2:def 1;
Q . (0. E) = 0. F by LOPBAN_7:3;
hence v = 0. E by A1, A2, A3, FUNCT_1:def 4; :: thesis: verum
end;
assume v = 0. E ; :: thesis: Q . v = 0. F
hence Q . v = 0. F by LOPBAN_7:3; :: thesis: verum