defpred S1[ set , set , set ] means for a, b being Vector of V st $1 = a + W & $2 = b + W holds
$3 = (a + b) + W;
set C = CosetSet (V,W);
A1:
now for A, B being Element of CosetSet (V,W) ex z being Element of CosetSet (V,W) st S1[A,B,z]let A,
B be
Element of
CosetSet (
V,
W);
ex z being Element of CosetSet (V,W) st S1[A,B,z]
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;
B in CosetSet (
V,
W)
;
then consider B1 being
Coset of
W such that A4:
B1 = B
;
consider b being
Vector of
V such that A5:
B1 = b + W
by VECTSP_4:def 6;
reconsider z =
(a + b) + W as
Coset of
W by VECTSP_4:def 6;
z in CosetSet (
V,
W)
;
then reconsider z =
z as
Element of
CosetSet (
V,
W) ;
take z =
z;
S1[A,B,z]thus
S1[
A,
B,
z]
verumproof
let a1,
b1 be
Vector of
V;
( A = a1 + W & B = b1 + W implies z = (a1 + b1) + W )
assume that A6:
A = a1 + W
and A7:
B = b1 + W
;
z = (a1 + b1) + W
a1 in a + W
by A2, A3, A6, VECTSP_4:44;
then consider w1 being
Vector of
V such that A8:
w1 in W
and A9:
a1 = a + w1
by VECTSP_4:42;
b1 in b + W
by A4, A5, A7, VECTSP_4:44;
then consider w2 being
Vector of
V such that A10:
w2 in W
and A11:
b1 = b + w2
by VECTSP_4:42;
A12:
w1 + w2 in W
by A8, A10, VECTSP_4:20;
a1 + b1 =
((w1 + a) + b) + w2
by A9, A11, RLVECT_1:def 3
.=
(w1 + (a + b)) + w2
by RLVECT_1:def 3
.=
(a + b) + (w1 + w2)
by RLVECT_1:def 3
;
then A13:
a1 + b1 in (a + b) + W
by A12;
a1 + b1 in (a1 + b1) + W
by VECTSP_4:44;
hence
z = (a1 + b1) + W
by A13, VECTSP_4:56;
verum
end; end;
consider f being Function of [:(CosetSet (V,W)),(CosetSet (V,W)):],(CosetSet (V,W)) such that
A14:
for A, B being Element of CosetSet (V,W) holds S1[A,B,f . (A,B)]
from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CosetSet (V,W)) ;
take
f
; for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f . (A,B) = (a + b) + W
let A, B be Element of CosetSet (V,W); for a, b being Vector of V st A = a + W & B = b + W holds
f . (A,B) = (a + b) + W
let a, b be Vector of V; ( A = a + W & B = b + W implies f . (A,B) = (a + b) + W )
assume
( A = a + W & B = b + W )
; f . (A,B) = (a + b) + W
hence
f . (A,B) = (a + b) + W
by A14; verum