let X be non empty set ; for x, y being Element of X
for f being Enumeration of X holds (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X
let x, y be Element of X; for f being Enumeration of X holds (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X
let f be Enumeration of X; (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X
set g = (f +* (x,(f . y))) +* (y,(f . x));
set A = dom ((f +* (x,(f . y))) +* (y,(f . x)));
A1:
dom (f +* (x,(f . y))) = dom f
by FUNCT_7:30;
A2:
dom ((f +* (x,(f . y))) +* (y,(f . x))) = dom (f +* (x,(f . y)))
by FUNCT_7:30;
A3:
dom f = X
by Th6;
A4:
rng f = card X
by Th6;
A5:
rng ((f +* (x,(f . y))) +* (y,(f . x))) = rng f
proof
{(f . x)} c= rng f
by A4, ZFMISC_1:31;
then A6:
(rng f) \/ {(f . x)} = rng f
by XBOOLE_1:12;
A7:
rng ((f +* (x,(f . y))) +* (y,(f . x))) c= (rng (f +* (x,(f . y)))) \/ {(f . x)}
by FUNCT_7:100;
{(f . y)} c= rng f
by A4, ZFMISC_1:31;
then
(rng f) \/ {(f . y)} = rng f
by XBOOLE_1:12;
then
(rng (f +* (x,(f . y)))) \/ {(f . x)} c= rng f
by A6, FUNCT_7:100, XBOOLE_1:9;
hence
rng ((f +* (x,(f . y))) +* (y,(f . x))) c= rng f
by A7;
XBOOLE_0:def 10 rng f c= rng ((f +* (x,(f . y))) +* (y,(f . x)))
let z be
object ;
TARSKI:def 3 ( not z in rng f or z in rng ((f +* (x,(f . y))) +* (y,(f . x))) )
assume
z in rng f
;
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))
then consider a being
object such that A8:
a in dom f
and A9:
z = f . a
by FUNCT_1:def 3;
per cases
( ( a <> x & a <> y ) or a = x or a = y )
;
suppose A10:
(
a <> x &
a <> y )
;
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))then A11:
((f +* (x,(f . y))) +* (y,(f . x))) . a = (f +* (x,(f . y))) . a
by FUNCT_7:32;
(f +* (x,(f . y))) . a = z
by A9, A10, FUNCT_7:32;
hence
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))
by A1, A2, A8, A11, FUNCT_1:def 3;
verum end; suppose
a = x
;
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))then
((f +* (x,(f . y))) +* (y,(f . x))) . y = z
by A1, A3, A9, FUNCT_7:31;
hence
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))
by A1, A2, A3, FUNCT_1:def 3;
verum end; suppose A12:
a = y
;
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))then A13:
(
x <> y implies
((f +* (x,(f . y))) +* (y,(f . x))) . x = (f +* (x,z)) . x )
by A9, FUNCT_7:32;
A14:
(f +* (x,z)) . x = z
by A3, FUNCT_7:31;
(
x = y implies
((f +* (x,(f . y))) +* (y,(f . x))) . x = z )
by A1, A3, A9, A12, FUNCT_7:31;
hence
z in rng ((f +* (x,(f . y))) +* (y,(f . x)))
by A1, A2, A3, A14, A13, FUNCT_1:def 3;
verum end; end;
end;
(f +* (x,(f . y))) +* (y,(f . x)) is one-to-one
proof
let a,
b be
object ;
FUNCT_1:def 4 ( not a in proj1 ((f +* (x,(f . y))) +* (y,(f . x))) or not b in proj1 ((f +* (x,(f . y))) +* (y,(f . x))) or not ((f +* (x,(f . y))) +* (y,(f . x))) . a = ((f +* (x,(f . y))) +* (y,(f . x))) . b or a = b )
A15:
(
a <> y implies
((f +* (x,(f . y))) +* (y,(f . x))) . a = (f +* (x,(f . y))) . a )
by FUNCT_7:32;
A16:
(
a <> x implies
(f +* (x,(f . y))) . a = f . a )
by FUNCT_7:32;
A17:
(
b = y implies
((f +* (x,(f . y))) +* (y,(f . x))) . b = f . x )
by A1, A3, FUNCT_7:31;
A18:
(
b <> y implies
((f +* (x,(f . y))) +* (y,(f . x))) . b = (f +* (x,(f . y))) . b )
by FUNCT_7:32;
A19:
(
b = x implies
(f +* (x,(f . y))) . b = f . y )
by A3, FUNCT_7:31;
A20:
(
a = x implies
(f +* (x,(f . y))) . a = f . y )
by A3, FUNCT_7:31;
A21:
(
b <> x implies
(f +* (x,(f . y))) . b = f . b )
by FUNCT_7:32;
(
a = y implies
((f +* (x,(f . y))) +* (y,(f . x))) . a = f . x )
by A1, A3, FUNCT_7:31;
hence
( not
a in proj1 ((f +* (x,(f . y))) +* (y,(f . x))) or not
b in proj1 ((f +* (x,(f . y))) +* (y,(f . x))) or not
((f +* (x,(f . y))) +* (y,(f . x))) . a = ((f +* (x,(f . y))) +* (y,(f . x))) . b or
a = b )
by A2, A3, A15, A20, A16, A17, A18, A19, A21, FUNCT_1:def 4;
verum
end;
hence
(f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X
by A1, A2, A3, A4, A5, Th6; verum