let D be non empty set ; for I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let I, J be non empty set ; for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let F, G be BinOp of D; for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let f be Function of I,D; for g being Function of J,D st F is commutative & F is associative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
let g be Function of J,D; ( F is commutative & F is associative implies for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g))))) )
assume A1:
( F is commutative & F is associative )
; for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
reconsider G = G as Function of [:D,D:],D ;
A2:
dom (G * (f,g)) = [:I,J:]
by FUNCT_2:def 1;
now for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))let x be
Element of
I;
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))let y be
Element of
J;
F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))A3:
[x,y] in [:I,J:]
by ZFMISC_1:87;
reconsider z =
g . y as
Element of
D ;
reconsider u =
[x,y] as
Element of
[:I,J:] by ZFMISC_1:87;
A4:
dom <:f,((dom f) --> z):> =
(dom f) /\ (dom ((dom f) --> z))
by FUNCT_3:def 7
.=
(dom f) /\ (dom f)
by FUNCOP_1:13
.=
dom f
;
(
rng f c= D &
rng ((dom f) --> z) c= D )
by RELAT_1:def 19;
then A5:
[:(rng f),(rng ((dom f) --> z)):] c= [:D,D:]
by ZFMISC_1:96;
dom f = I
by FUNCT_2:def 1;
then A6:
x in dom <:f,((dom f) --> z):>
by A4;
(
dom G = [:D,D:] &
rng <:f,((dom f) --> z):> c= [:(rng f),(rng ((dom f) --> z)):] )
by FUNCT_2:def 1, FUNCT_3:51;
then
x in dom (G * <:f,((dom f) --> z):>)
by A6, A5, RELAT_1:27, XBOOLE_1:1;
then A7:
x in dom (G [:] (f,z))
by FUNCOP_1:def 4;
A8:
F $$ (
{.x.},
(G [:] (f,(F $$ ({.y.},g))))) =
(G [:] (f,(F $$ ({.y.},g)))) . x
by A1, SETWISEO:17
.=
(G [:] (f,(g . y))) . x
by A1, SETWISEO:17
.=
G . (
(f . x),
(g . y))
by A7, FUNCOP_1:27
;
F $$ (
[:{.x.},{.y.}:],
(G * (f,g))) =
F $$ (
{.u.},
(G * (f,g)))
by ZFMISC_1:29
.=
(G * (f,g)) . (
x,
y)
by A1, SETWISEO:17
.=
G . (
(f . x),
(g . y))
by A2, A3, FINSEQOP:77
;
hence
F $$ (
[:{.x.},{.y.}:],
(G * (f,g)))
= F $$ (
{.x.},
(G [:] (f,(F $$ ({.y.},g)))))
by A8;
verum end;
hence
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))
; verum