set cF = INT ;
set C = CosetSet (V,W);
let f1, f2 be Function of [:INT,(CosetSet (V,W)):],(CosetSet (V,W)); :: thesis: ( ( for z being Integer
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 Integer
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
A8: for z being Integer
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
A9: for z being Integer
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 :: thesis: for z being Element of INT
for A being Element of CosetSet (V,W) holds f1 . (z,A) = f2 . (z,A)

let z be Element of INT ; :: 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
A10: A1 = A ;
consider a being VECTOR of V such that
A11: A1 = a + W by ZMODUL01:def 13;
thus f1 . (z,A) = (z * a) + W by A8, A10, A11
.= f2 . (z,A) by A9, A10, A11 ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum