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:32;
A2: dom ((f +* x,(f . y)) +* y,(f . x)) = dom (f +* x,(f . y)) by FUNCT_7:32;
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:37;
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:102;
{(f . y)} c= rng f by A4, ZFMISC_1:37;
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:102, XBOOLE_1:9;
hence rng ((f +* x,(f . y)) +* y,(f . x)) c= rng f by A7, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng ((f +* x,(f . y)) +* y,(f . x))
let z be set ; :: 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 set such that
A8: a in dom f and
A9: z = f . a by FUNCT_1:def 5;

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:34;
(f +* x,(f . y)) . a = z by A9, A10, FUNCT_7:34;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, A2, A8, A11, FUNCT_1:def 5; :: 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:33;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, A2, A3, FUNCT_1:def 5; :: 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:34;
A14: (f +* x,z) . x = z by A3, FUNCT_7:33;
( x = y implies ((f +* x,(f . y)) +* y,(f . x)) . x = z ) by A1, A3, A9, A12, FUNCT_7:33;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, A2, A3, A14, A13, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

(f +* x,(f . y)) +* y,(f . x) is one-to-one

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: 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:34;
A16: ( a <> x implies (f +* x,(f . y)) . a = f . a ) by FUNCT_7:34;
A17: ( b = y implies ((f +* x,(f . y)) +* y,(f . x)) . b = f . x ) by A1, A3, FUNCT_7:33;
A18: ( b <> y implies ((f +* x,(f . y)) +* y,(f . x)) . b = (f +* x,(f . y)) . b ) by FUNCT_7:34;
A19: ( b = x implies (f +* x,(f . y)) . b = f . y ) by A3, FUNCT_7:33;
A20: ( a = x implies (f +* x,(f . y)) . a = f . y ) by A3, FUNCT_7:33;
A21: ( b <> x implies (f +* x,(f . y)) . b = f . b ) by FUNCT_7:34;
( a = y implies ((f +* x,(f . y)) +* y,(f . x)) . a = f . x ) by A1, A3, FUNCT_7:33;
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 8; :: thesis: verum

end;

hence (f +* x,(f . y)) +* y,(f . x) is Enumeration of X by A1, A2, A3, A4, A5, Th6; :: thesis: verum