deffunc H1( set , set ) -> set = [$2,$1];
let I, J, D 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
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
let F, G be BinOp of D; for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
let f be Function of I,D; for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
let g be Function of J,D; for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
let X be Element of Fin I; for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
let Y be Element of Fin J; ( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative implies F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f) )
assume A1:
( F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) )
; ( not G is commutative or F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f) )
consider h being Function such that
A2:
( dom h = [:J,I:] & ( for x, y being set st x in J & y in I holds
h . x,y = H1(x,y) ) )
from FUNCT_3:sch 2();
now let z1,
z2 be
set ;
( z1 in dom h & z2 in dom h & h . z1 = h . z2 implies z1 = z2 )assume that A3:
z1 in dom h
and A4:
z2 in dom h
and A5:
h . z1 = h . z2
;
z1 = z2consider x2,
y2 being
set such that A6:
z2 = [x2,y2]
by A2, A4, RELAT_1:def 1;
(
x2 in J &
y2 in I )
by A2, A4, A6, ZFMISC_1:106;
then A7:
h . x2,
y2 = [y2,x2]
by A2;
consider x1,
y1 being
set such that A8:
z1 = [x1,y1]
by A2, A3, RELAT_1:def 1;
(
x1 in J &
y1 in I )
by A2, A3, A8, ZFMISC_1:106;
then A9:
h . x1,
y1 = [y1,x1]
by A2;
then
y1 = y2
by A5, A8, A6, A7, ZFMISC_1:33;
hence
z1 = z2
by A5, A8, A6, A9, A7, ZFMISC_1:33;
verum end;
then A10:
h is one-to-one
by FUNCT_1:def 8;
A11:
for x being set st x in [:J,I:] holds
h . x in [:I,J:]
proof
let x be
set ;
( x in [:J,I:] implies h . x in [:I,J:] )
assume A12:
x in [:J,I:]
;
h . x in [:I,J:]
then consider y,
z being
set such that A13:
x = [y,z]
by RELAT_1:def 1;
A14:
(
y in J &
z in I )
by A12, A13, ZFMISC_1:106;
then
h . y,
z = [z,y]
by A2;
hence
h . x in [:I,J:]
by A13, A14, ZFMISC_1:106;
verum
end;
assume A15:
G is commutative
; F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
A16:
G * g,f = (G * f,g) * h
proof
reconsider G =
G as
Function of
[:D,D:],
D ;
A17:
dom (G * g,f) = [:J,I:]
by FUNCT_2:def 1;
A18:
dom (G * f,g) = [:I,J:]
by FUNCT_2:def 1;
A19:
for
x being
set holds
(
x in dom (G * g,f) iff (
x in dom h &
h . x in dom (G * f,g) ) )
proof
let x be
set ;
( x in dom (G * g,f) iff ( x in dom h & h . x in dom (G * f,g) ) )
thus
(
x in dom (G * g,f) implies (
x in dom h &
h . x in dom (G * f,g) ) )
( x in dom h & h . x in dom (G * f,g) implies x in dom (G * g,f) )proof
assume A20:
x in dom (G * g,f)
;
( x in dom h & h . x in dom (G * f,g) )
then consider y,
z being
set such that A21:
x = [y,z]
by RELAT_1:def 1;
A22:
(
y in J &
z in I )
by A17, A20, A21, ZFMISC_1:106;
then
h . y,
z = [z,y]
by A2;
hence
(
x in dom h &
h . x in dom (G * f,g) )
by A2, A18, A21, A22, ZFMISC_1:106;
verum
end;
assume that A23:
x in dom h
and
h . x in dom (G * f,g)
;
x in dom (G * g,f)
thus
x in dom (G * g,f)
by A2, A23, FUNCT_2:def 1;
verum
end;
for
x being
set st
x in dom (G * g,f) holds
(G * g,f) . x = (G * f,g) . (h . x)
proof
let x be
set ;
( x in dom (G * g,f) implies (G * g,f) . x = (G * f,g) . (h . x) )
assume A24:
x in dom (G * g,f)
;
(G * g,f) . x = (G * f,g) . (h . x)
then consider y,
z being
set such that A25:
x = [y,z]
by RELAT_1:def 1;
reconsider z =
z as
Element of
I by A17, A24, A25, ZFMISC_1:106;
reconsider y =
y as
Element of
J by A17, A24, A25, ZFMISC_1:106;
A26:
[z,y] in dom (G * f,g)
by A18, ZFMISC_1:106;
A27:
[y,z] in dom (G * g,f)
by A17, ZFMISC_1:106;
thus (G * f,g) . (h . x) =
(G * f,g) . (h . y,z)
by A25
.=
(G * f,g) . z,
y
by A2
.=
G . (f . z),
(g . y)
by A26, FINSEQOP:82
.=
G . (g . y),
(f . z)
by A15, BINOP_1:def 2
.=
(G * g,f) . y,
z
by A27, FINSEQOP:82
.=
(G * g,f) . x
by A25
;
verum
end;
hence
G * g,
f = (G * f,g) * h
by A19, FUNCT_1:20;
verum
end;
A28:
( X c= I & Y c= J )
by FINSUB_1:def 5;
for y being set holds
( y in [:X,Y:] iff y in h .: [:Y,X:] )
proof
let y be
set ;
( y in [:X,Y:] iff y in h .: [:Y,X:] )
thus
(
y in [:X,Y:] implies
y in h .: [:Y,X:] )
( y in h .: [:Y,X:] implies y in [:X,Y:] )proof
assume A29:
y in [:X,Y:]
;
y in h .: [:Y,X:]
then consider y1,
x1 being
set such that A30:
y = [y1,x1]
by RELAT_1:def 1;
A31:
(
y1 in X &
x1 in Y )
by A29, A30, ZFMISC_1:106;
then A32:
(
[x1,y1] in [:Y,X:] &
[x1,y1] in dom h )
by A28, A2, ZFMISC_1:106;
h . x1,
y1 = y
by A28, A2, A30, A31;
hence
y in h .: [:Y,X:]
by A32, FUNCT_1:def 12;
verum
end;
assume
y in h .: [:Y,X:]
;
y in [:X,Y:]
then consider x being
set such that
x in dom h
and A33:
x in [:Y,X:]
and A34:
y = h . x
by FUNCT_1:def 12;
consider x1,
y1 being
set such that A35:
x = [x1,y1]
by A33, RELAT_1:def 1;
A36:
(
x1 in Y &
y1 in X )
by A33, A35, ZFMISC_1:106;
y = h . x1,
y1
by A34, A35;
then
y = [y1,x1]
by A28, A2, A36;
hence
y in [:X,Y:]
by A36, ZFMISC_1:106;
verum
end;
then A37:
h .: [:Y,X:] = [:X,Y:]
by TARSKI:2;
reconsider h = h as Function of [:J,I:],[:I,J:] by A2, A11, FUNCT_2:5;
F $$ [:X,Y:],(G * f,g) =
F $$ [:Y,X:],((G * f,g) * h)
by A1, A10, A37, SETWOP_2:8
.=
F $$ [:Y,X:],(G * g,f)
by A16
;
hence
F $$ [:X,Y:],(G * f,g) = F $$ [:Y,X:],(G * g,f)
; verum