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 & dom ((f +* x,(f . y)) +* y,(f . x)) = dom (f +* x,(f . y)) & dom f = X & rng f = card X ) by ThNum1, FUNCT_7:32;
A2: rng ((f +* x,(f . y)) +* y,(f . x)) = rng f

proof

( {(f . y)} c= rng f & {(f . x)} c= rng f ) by A1, ZFMISC_1:37;
then A4: ( rng ((f +* x,(f . y)) +* y,(f . x)) c= (rng (f +* x,(f . y))) \/ {(f . x)} & (rng f) \/ {(f . y)} = rng f & (rng f) \/ {(f . x)} = rng f & rng (f +* x,(f . y)) c= (rng f) \/ {(f . y)} ) by FUNCT_7:102, XBOOLE_1:12;
then (rng (f +* x,(f . y))) \/ {(f . x)} c= rng f by XBOOLE_1:9;
hence rng ((f +* x,(f . y)) +* y,(f . x)) c= rng f by A4, 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
A6: ( a in dom f & z = f . a ) by FUNCT_1:def 5;

per cases ( ( a <> x & a <> y ) or a = x or a = y ) ;

suppose ( a <> x & a <> y ) ; :: thesis: z in rng ((f +* x,(f . y)) +* y,(f . x))

then ( ((f +* x,(f . y)) +* y,(f . x)) . a = (f +* x,(f . y)) . a & (f +* x,(f . y)) . a = z ) by A6, FUNCT_7:34;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, A6, 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, A6, FUNCT_7:33;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, FUNCT_1:def 5; :: thesis: verum

end;

suppose a = y ; :: thesis: z in rng ((f +* x,(f . y)) +* y,(f . x))

then ( ( x = y implies ((f +* x,(f . y)) +* y,(f . x)) . x = z ) & (f +* x,z) . x = z & ( x <> y implies ((f +* x,(f . y)) +* y,(f . x)) . x = (f +* x,z) . x ) ) by A1, A6, FUNCT_7:33, FUNCT_7:34;
hence z in rng ((f +* x,(f . y)) +* y,(f . x)) by A1, 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 dom ((f +* x,(f . y)) +* y,(f . x)) or not b in dom ((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 )
A3: ( ( a = y implies ((f +* x,(f . y)) +* y,(f . x)) . a = f . x ) & ( a <> y implies ((f +* x,(f . y)) +* y,(f . x)) . a = (f +* x,(f . y)) . a ) & ( a = x implies (f +* x,(f . y)) . a = f . y ) & ( a <> x implies (f +* x,(f . y)) . a = f . a ) ) by A1, FUNCT_7:33, FUNCT_7:34;
( ( b = y implies ((f +* x,(f . y)) +* y,(f . x)) . b = f . x ) & ( b <> y implies ((f +* x,(f . y)) +* y,(f . x)) . b = (f +* x,(f . y)) . b ) & ( b = x implies (f +* x,(f . y)) . b = f . y ) & ( b <> x implies (f +* x,(f . y)) . b = f . b ) ) by A1, FUNCT_7:33, FUNCT_7:34;
hence ( not a in dom ((f +* x,(f . y)) +* y,(f . x)) or not b in dom ((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 A1, A3, FUNCT_1:def 8; :: thesis: verum

end;

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