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_{1} being object st

( x in K82((f *')) & b_{1} in K82((f *')) & not (f *') . x = (f *') . b_{1} )

take y ; :: thesis: ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y )

hence ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y ) by A1, Def2; :: thesis: verum

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

( x in K82((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) *'

then
( dom (f *') = the carrier of V & (f *') . x <> (f . w) *' )
by Def2, FUNCT_2:def 1;assume
(f . v) *' = (f . w) *'
; :: thesis: contradiction

then f . v = ((f . w) *') *' ;

hence contradiction by A3; :: thesis: verum

end;then f . v = ((f . w) *') *' ;

hence contradiction by A3; :: thesis: verum

hence ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y ) by A1, Def2; :: thesis: verum