let D be non empty set ; for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let I, J be non empty set ; for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let F be BinOp of D; for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let f be Function of [:I,J:],D; for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let g be Function of I,D; for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
let Y be Element of Fin J; ( F is having_a_unity & F is commutative & F is associative implies for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g) )
assume that
A1:
F is having_a_unity
and
A2:
( F is commutative & F is associative )
; for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
now for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)let x be
Element of
I;
( ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) implies F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g) )assume A3:
for
i being
Element of
I holds
g . i = F $$ (
Y,
((curry f) . i))
;
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)deffunc H1(
object )
-> object =
[x,$1];
consider h being
Function such that A4:
(
dom h = J & ( for
y being
object st
y in J holds
h . y = H1(
y) ) )
from FUNCT_1:sch 3();
A5:
(
dom ((curry f) . x) = J &
dom (f * h) = J &
rng h c= [:I,J:] )
A9:
for
y being
object st
y in J holds
((curry f) . x) . y = (f * h) . y
for
y being
object holds
(
y in [:{x},Y:] iff
y in h .: Y )
proof
let y be
object ;
( y in [:{x},Y:] iff y in h .: Y )
thus
(
y in [:{x},Y:] implies
y in h .: Y )
( y in h .: Y implies y in [:{x},Y:] )proof
assume A12:
y in [:{x},Y:]
;
y in h .: Y
then consider y1,
x1 being
object such that A13:
y = [y1,x1]
by RELAT_1:def 1;
A14:
y1 in {x}
by A12, A13, ZFMISC_1:87;
A15:
(
Y c= J &
x1 in Y )
by A12, A13, FINSUB_1:def 5, ZFMISC_1:87;
then h . x1 =
[x,x1]
by A4
.=
y
by A13, A14, TARSKI:def 1
;
hence
y in h .: Y
by A4, A15, FUNCT_1:def 6;
verum
end;
assume
y in h .: Y
;
y in [:{x},Y:]
then consider z being
object such that A16:
z in dom h
and A17:
z in Y
and A18:
y = h . z
by FUNCT_1:def 6;
y = [x,z]
by A4, A16, A18;
hence
y in [:{x},Y:]
by A17, ZFMISC_1:105;
verum
end; then A19:
h .: Y = [:{x},Y:]
by TARSKI:2;
then A23:
h is
one-to-one
by FUNCT_1:def 4;
reconsider h =
h as
Function of
J,
[:I,J:] by A4, A5, FUNCT_2:2;
thus F $$ (
[:{.x.},Y:],
f) =
F $$ (
Y,
(f * h))
by A1, A2, A23, A19, SETWOP_2:6
.=
F $$ (
Y,
((curry f) . x))
by A5, A9, FUNCT_1:2
.=
g . x
by A3
.=
F $$ (
{.x.},
g)
by A2, SETWISEO:17
;
verum end;
hence
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
; verum