consider x, y being object such that
A1: x in dom f and
A2: y in dom f and
A3: f . x <> f . y by FUNCT_1:def 10;
reconsider v = x, w = y as Vector of V by A1, A2;
take x ; :: according to FUNCT_1:def 10 :: thesis: ex b₁ being object st
( x in K82((f *')) & b₁ in K82((f *')) & not (f *') . x = (f *') . b₁ )
take y ; :: thesis: ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y )

now :: thesis: not (f . v) *' = (f . w) *'

assume (f . v) *' = (f . w) *' ; :: thesis: contradiction
then f . v = ((f . w) *') *' ;
hence contradiction by A3; :: thesis: verum

end;

then ( dom (f *') = the carrier of V & (f *') . x <> (f . w) *' ) by Def2, FUNCT_2:def 1;
hence ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y ) by A1, Def2; :: thesis: verum