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_{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 )

consider vx being Vector of V, wx being Vector of W such that

A6: x = [vx,wx] by A2, DOMAIN_1: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

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

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: verumassume
(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;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