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

end;

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