let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty Subset of U
for f being Function of B,V st f is one-to-one holds
for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)}
let U, V be VectSp of F; :: thesis: for B being non empty Subset of U
for f being Function of B,V st f is one-to-one holds
for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)}
let B be non empty Subset of U; :: thesis: for f being Function of B,V st f is one-to-one holds
for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)}
let f be Function of B,V; :: thesis: ( f is one-to-one implies for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)} )
assume A: f is one-to-one ; :: thesis: for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)}
let v be Element of V; :: thesis: ( v in rng f implies f " {v} = {((f ") . v)} )
assume v in rng f ; :: thesis: f " {v} = {((f ") . v)}
then consider x being object such that
B: f " {v} = {x} by A, FUNCT_1:74;
x in f " {v} by B, TARSKI:def 1;
then C: ( x in dom f & f . x in {v} ) by FUNCT_1:def 7;
then v = f . x by TARSKI:def 1;
hence f " {v} = {((f ") . v)} by B, A, C, FUNCT_1:34; :: thesis: verum