let X be non empty set ; :: thesis: 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; :: thesis: for f being Enumeration of X holds (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X
let f be Enumeration of X; :: thesis: (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; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng ((f +* (x,(f . y))) +* (y,(f . x)))
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in rng ((f +* (x,(f . y))) +* (y,(f . x))) )
assume z in rng f ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum
end;
suppose a = x ; :: thesis: 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; :: thesis: verum
end;
suppose A12: a = y ; :: thesis: 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; :: thesis: verum
end;
end;
end;
(f +* (x,(f . y))) +* (y,(f . x)) is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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; :: thesis: verum
end;
hence (f +* (x,(f . y))) +* (y,(f . x)) is Enumeration of X by A1, A2, A3, A4, A5, Th6; :: thesis: verum