set x = the Element of X;
deffunc H1( Element of X, Element of X) -> Element of X = IFEQ (X, the Element of X,c2,X);
( ex f being Function of (2 -tuples_on X),X st
for x, y being Element of X holds f . <*x,y*> = H1(x,y) & ( for f1, f2 being Function of (2 -tuples_on X),X st ( for x, y being Element of X holds f1 . <*x,y*> = H1(x,y) ) & ( for x, y being Element of X holds f2 . <*x,y*> = H1(x,y) ) holds
f1 = f2 ) )
from CIRCCMB3:sch 7();
then consider f being Function of (2 -tuples_on X),X such that
A1:
for a, b being Element of X holds f . <*a,b*> = IFEQ (a, the Element of X,b,a)
;
A2:
rng f c= X
;
A3:
dom f = 2 -tuples_on X
by FUNCT_2:def 1;
then reconsider f = f as non empty homogeneous PartFunc of (X *),X by A2, COMPUT_1:16, FINSEQ_2:134, RELSET_1:4;
arity f = 2
by A3, COMPUT_1:24;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (X *),X by A3, COMPUT_1:22;
take
f
; ( f is 2 -ary & f is associative & f is unital )
thus
arity f = 2
by A3, COMPUT_1:24; COMPUT_1:def 21 ( f is associative & f is unital )
hereby AOFA_000:def 2 f is unital
let u,
y,
z be
set ;
( <*u,y*> in dom f & <*y,z*> in dom f & <*(f . <*u,y*>),z*> in dom f & <*u,(f . <*y,z*>)*> in dom f implies f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*> )assume that A4:
<*u,y*> in dom f
and A5:
<*y,z*> in dom f
;
( <*(f . <*u,y*>),z*> in dom f & <*u,(f . <*y,z*>)*> in dom f implies f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*> )reconsider u9 =
u,
y9 =
y,
z9 =
z as
Element of
X by A3, A4, A5, FINSEQ_2:138;
assume that
<*(f . <*u,y*>),z*> in dom f
and
<*u,(f . <*y,z*>)*> in dom f
;
f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*>A6:
(
u = the
Element of
X implies
IFEQ (
u, the
Element of
X,
y,
u)
= y )
by FUNCOP_1:def 8;
A7:
(
u <> the
Element of
X implies
IFEQ (
u, the
Element of
X,
y,
u)
= u )
by FUNCOP_1:def 8;
A8:
(
u = the
Element of
X implies
IFEQ (
u, the
Element of
X,
(IFEQ (y, the Element of X,z,y)),
u)
= IFEQ (
y, the
Element of
X,
z,
y) )
by FUNCOP_1:def 8;
A9:
(
u <> the
Element of
X implies
IFEQ (
u, the
Element of
X,
(IFEQ (y, the Element of X,z,y)),
u)
= u )
by FUNCOP_1:def 8;
A10:
(
u <> the
Element of
X implies
IFEQ (
u, the
Element of
X,
z,
u)
= u )
by FUNCOP_1:def 8;
thus f . <*(f . <*u,y*>),z*> =
f . <*(IFEQ (u9, the Element of X,y9,u9)),z9*>
by A1
.=
IFEQ (
(IFEQ (u, the Element of X,y,u)), the
Element of
X,
z,
(IFEQ (u, the Element of X,y,u)))
by A1
.=
f . <*u9,(IFEQ (y9, the Element of X,z9,y9))*>
by A1, A6, A7, A8, A9, A10
.=
f . <*u,(f . <*y,z*>)*>
by A1
;
verum
end;
take
the Element of X
; AOFA_000:def 3 the Element of X is_a_unity_wrt f
let y, z be set ; AOFA_000:def 1 ( ( <*y,z*> in dom f or <*z,y*> in dom f ) implies ( <* the Element of X,y*> in dom f & f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y ) )
assume
( <*y,z*> in dom f or <*z,y*> in dom f )
; ( <* the Element of X,y*> in dom f & f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
then reconsider y9 = y as Element of X by A3, FINSEQ_2:138;
<* the Element of X,y9*> in 2 -tuples_on X
by FINSEQ_2:137;
hence
<* the Element of X,y*> in dom f
by FUNCT_2:def 1; ( f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
thus f . <* the Element of X,y*> =
IFEQ ( the Element of X, the Element of X,y9, the Element of X)
by A1
.=
y
by FUNCOP_1:def 8
; ( <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
<*y9, the Element of X*> in 2 -tuples_on X
by FINSEQ_2:137;
hence
<*y, the Element of X*> in dom f
by FUNCT_2:def 1; f . <*y, the Element of X*> = y
A11:
( the Element of X = y or the Element of X <> y )
;
thus f . <*y, the Element of X*> =
IFEQ (y9, the Element of X, the Element of X,y9)
by A1
.=
y
by A11, FUNCOP_1:def 8
; verum