A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
consider x, y being object such that
A2: x in dom f and
A3: y in dom f and
A4: f . x <> f . y by FUNCT_1:def 10;
consider vy being Vector of V, wy being Vector of W such that
A5: y = [vy,wy] by A3, DOMAIN_1:1;
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 )
consider vx being Vector of V, wx being Vector of W such that
A6: x = [vx,wx] by A2, DOMAIN_1:1;

now :: thesis: not (f *') . (vx,wx) = (f *') . (vy,wy)

assume (f *') . (vx,wx) = (f *') . (vy,wy) ; :: thesis: contradiction
then ((f . (vx,wx)) *') *' = ((f *') . (vy,wy)) *' by Def8;
then f . (vx,wx) = ((f . (vy,wy)) *') *' by Def8;
hence contradiction by A4, A6, A5; :: thesis: verum

end;

hence ( x in K82((f *')) & y in K82((f *')) & not (f *') . x = (f *') . y ) by A2, A3, A1, A6, A5, FUNCT_2:def 1; :: thesis: verum