set cF = the carrier of K;
set C = CosetSet (V,W);
let f1, f2 be Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)); ( ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f1 . (z,A) = (z * a) + W ) & ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f2 . (z,A) = (z * a) + W ) implies f1 = f2 )
assume that
A7:
for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f1 . (z,A) = (z * a) + W
and
A8:
for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f2 . (z,A) = (z * a) + W
; f1 = f2
set C = CosetSet (V,W);
now for z being Element of K
for A being Element of CosetSet (V,W) holds f1 . (z,A) = f2 . (z,A)let z be
Element of
K;
for A being Element of CosetSet (V,W) holds f1 . (z,A) = f2 . (z,A)let A be
Element of
CosetSet (
V,
W);
f1 . (z,A) = f2 . (z,A)
A in CosetSet (
V,
W)
;
then consider A1 being
Coset of
W such that A9:
A1 = A
;
consider a being
Vector of
V such that A10:
A1 = a + W
by VECTSP_4:def 6;
thus f1 . (
z,
A) =
(z * a) + W
by A7, A9, A10
.=
f2 . (
z,
A)
by A8, A9, A10
;
verum end;
hence
f1 = f2
by BINOP_1:2; verum