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
; FUNCT_1:def 10 ex b1 being object st
( x in K82((f *')) & b1 in K82((f *')) & not (f *') . x = (f *') . b1 )
take
y
; ( 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 not (f *') . (vx,wx) = (f *') . (vy,wy)assume
(f *') . (
vx,
wx)
= (f *') . (
vy,
wy)
;
contradictionthen
((f . (vx,wx)) *') *' = ((f *') . (vy,wy)) *'
by Def8;
then
f . (
vx,
wx)
= ((f . (vy,wy)) *') *'
by Def8;
hence
contradiction
by A4, A6, A5;
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; verum