defpred S1[ set , set , set ] means for a, b being PartFunc of X,COMPLEX st a in $1 & b in $2 holds
$3 = a.e-Ceq-class ((a + b),M);
set C = CCosetSet M;
A1:
now for A, B being Element of CCosetSet M ex z being Element of CCosetSet M st S1[A,B,z]let A,
B be
Element of
CCosetSet M;
ex z being Element of CCosetSet M st S1[A,B,z]
A in CCosetSet M
;
then consider a being
PartFunc of
X,
COMPLEX such that A2:
A = a.e-Ceq-class (
a,
M)
and A3:
a in L1_CFunctions M
;
B in CCosetSet M
;
then consider b being
PartFunc of
X,
COMPLEX such that A4:
B = a.e-Ceq-class (
b,
M)
and A5:
b in L1_CFunctions M
;
set z =
a.e-Ceq-class (
(a + b),
M);
A6:
a + b in L1_CFunctions M
by A3, A5, Th17;
then
a.e-Ceq-class (
(a + b),
M)
in CCosetSet M
;
then reconsider z =
a.e-Ceq-class (
(a + b),
M) as
Element of
CCosetSet M ;
take z =
z;
S1[A,B,z]now for a1, b1 being PartFunc of X,COMPLEX st a1 in A & b1 in B holds
z = a.e-Ceq-class ((a1 + b1),M)let a1,
b1 be
PartFunc of
X,
COMPLEX;
( a1 in A & b1 in B implies z = a.e-Ceq-class ((a1 + b1),M) )assume A7:
(
a1 in A &
b1 in B )
;
z = a.e-Ceq-class ((a1 + b1),M)then
(
a1 a.e.cpfunc= a,
M &
b1 a.e.cpfunc= b,
M )
by A2, A3, A4, A5, Th30;
then A8:
a1 + b1 a.e.cpfunc= a + b,
M
by Th25;
a1 + b1 in L1_CFunctions M
by A7, Th17;
hence
z = a.e-Ceq-class (
(a1 + b1),
M)
by A6, A8, Th32;
verum end; hence
S1[
A,
B,
z]
;
verum end;
consider f being Function of [:(CCosetSet M),(CCosetSet M):],(CCosetSet M) such that
A9:
for A, B being Element of CCosetSet M holds S1[A,B,f . (A,B)]
from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CCosetSet M) ;
take
f
; for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f . (A,B) = a.e-Ceq-class ((a + b),M)
let A, B be Element of CCosetSet M; for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f . (A,B) = a.e-Ceq-class ((a + b),M)
let a, b be PartFunc of X,COMPLEX; ( a in A & b in B implies f . (A,B) = a.e-Ceq-class ((a + b),M) )
assume
( a in A & b in B )
; f . (A,B) = a.e-Ceq-class ((a + b),M)
hence
f . (A,B) = a.e-Ceq-class ((a + b),M)
by A9; verum