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); :: thesis: ( ( 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 ; :: thesis: f1 = f2
set C = CosetSet V,W;

now

let z be Element of K; :: thesis: for A being Element of CosetSet V,W holds f1 . z,A = f2 . z,A
let A be Element of CosetSet V,W; :: thesis: 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 ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum