defpred S1[ Element of K, set , set ] means for a being Vector of V st $2 = a + W holds
$3 = ($1 * a) + W;
set cF = the carrier of K;
set C = CosetSet (V,W);
A1:
now for z being Element of K
for A being Element of CosetSet (V,W) ex c being Element of CosetSet (V,W) st S1[z,A,c]let z be
Element of
K;
for A being Element of CosetSet (V,W) ex c being Element of CosetSet (V,W) st S1[z,A,c]let A be
Element of
CosetSet (
V,
W);
ex c being Element of CosetSet (V,W) st S1[z,A,c]
A in CosetSet (
V,
W)
;
then consider A1 being
Coset of
W such that A2:
A1 = A
;
consider a being
Vector of
V such that A3:
A1 = a + W
by VECTSP_4:def 6;
reconsider c =
(z * a) + W as
Coset of
W by VECTSP_4:def 6;
c in CosetSet (
V,
W)
;
then reconsider c =
c as
Element of
CosetSet (
V,
W) ;
take c =
c;
S1[z,A,c]thus
S1[
z,
A,
c]
verum end;
consider f being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) such that
A6:
for z being Element of K
for A being Element of CosetSet (V,W) holds S1[z,A,f . (z,A)]
from BINOP_1:sch 3(A1);
take
f
; 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
f . (z,A) = (z * a) + W
let z be Element of K; for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let A be Element of CosetSet (V,W); for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let a be Vector of V; ( A = a + W implies f . (z,A) = (z * a) + W )
assume
A = a + W
; f . (z,A) = (z * a) + W
hence
f . (z,A) = (z * a) + W
by A6; verum