A1: dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
consider x, y being set such that
A2: x in dom f and
A3: y in dom f and
A4: f . x <> f . y by FUNCT_1:def 16;
consider vy being Vector of V, wy being Vector of W such that
A5: y = [vy,wy] by A3, DOMAIN_1:9;
take x ; :: according to FUNCT_1:def 16 :: thesis: ex b₁ being set st
( x in K65((f *' )) & b₁ in K65((f *' )) & not (f *' ) . x = (f *' ) . b₁ )
take y ; :: thesis: ( x in K65((f *' )) & y in K65((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:9;

now

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 K65((f *' )) & y in K65((f *' )) & not (f *' ) . x = (f *' ) . y ) by A2, A3, A1, A6, A5, FUNCT_2:def 1; :: thesis: verum