let x, y be object ; :: thesis: for F being finite set
for E being Enumeration of F st not y in union F holds
Swap (E,x,y) is Enumeration of swap (F,x,y)
let F be finite set ; :: thesis: for E being Enumeration of F st not y in union F holds
Swap (E,x,y) is Enumeration of swap (F,x,y)
let E be Enumeration of F; :: thesis: ( not y in union F implies Swap (E,x,y) is Enumeration of swap (F,x,y) )
assume A1: not y in union F ; :: thesis: Swap (E,x,y) is Enumeration of swap (F,x,y)
set S = Swap (E,x,y);
A2: ( dom (Swap (E,x,y)) = dom E & dom E = Seg (len E) ) by Def4, FINSEQ_1:def 3;
A3: rng E = F by RLAFFIN3:def 1;
A4: rng (Swap (E,x,y)) c= swap (F,x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (Swap (E,x,y)) or a in swap (F,x,y) )
assume a in rng (Swap (E,x,y)) ; :: thesis: a in swap (F,x,y)
then consider c being object such that
A5: ( c in dom (Swap (E,x,y)) & (Swap (E,x,y)) . c = a ) by FUNCT_1:def 3;
A6: E . c in rng E by A5, A2, FUNCT_1:def 3;

per cases ( x in E . c or not x in E . c ) ;

suppose A7: x in E . c ; :: thesis: a in swap (F,x,y)

then (Swap (E,x,y)) . c = ((E . c) \ {x}) \/ {y} by A5, A2, Def4;
then (Swap (E,x,y)) . c in { ((A \ {x}) \/ {y}) where A is Element of F : x in A } by A7, A6;
hence a in swap (F,x,y) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: not x in E . c ; :: thesis: a in swap (F,x,y)

then (Swap (E,x,y)) . c = (E . c) \/ {x} by A5, A2, Def4;
then (Swap (E,x,y)) . c in { (A \/ {x}) where A is Element of F : ( not x in A & A in F ) } by A8, A6;
hence a in swap (F,x,y) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

swap (F,x,y) c= rng (Swap (E,x,y))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in swap (F,x,y) or a in rng (Swap (E,x,y)) )
assume a in swap (F,x,y) ; :: thesis: a in rng (Swap (E,x,y))

per cases then ( a in { ((A \ {x}) \/ {y}) where A is Element of F : x in A } or a in { (A \/ {x}) where A is Element of F : ( not x in A & A in F ) } ) by XBOOLE_0:def 3;

suppose a in { ((A \ {x}) \/ {y}) where A is Element of F : x in A } ; :: thesis: a in rng (Swap (E,x,y))

then consider A being Element of F such that
A9: ( a = (A \ {x}) \/ {y} & x in A ) ;
F <> {} by A9, SUBSET_1:def 1;
then consider b being object such that
A10: ( b in dom E & E . b = A ) by A3, FUNCT_1:def 3;
(Swap (E,x,y)) . b = ((E . b) \ {x}) \/ {y} by Def4, A9, A10;
hence a in rng (Swap (E,x,y)) by A9, A10, A2, FUNCT_1:def 3; :: thesis: verum

end;

suppose a in { (A \/ {x}) where A is Element of F : ( not x in A & A in F ) } ; :: thesis: a in rng (Swap (E,x,y))

then consider A being Element of F such that
A11: ( a = A \/ {x} & not x in A & A in F ) ;
consider b being object such that
A12: ( b in dom E & E . b = A ) by A11, A3, FUNCT_1:def 3;
(Swap (E,x,y)) . b = (E . b) \/ {x} by Def4, A11, A12;
hence a in rng (Swap (E,x,y)) by A11, A12, A2, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then A13: swap (F,x,y) = rng (Swap (E,x,y)) by A4;
A14: card (swap (F,x,y)) = card F by A1, Th11;
( card F = len E & len E = len (Swap (E,x,y)) ) by CARD_1:def 7;
then Swap (E,x,y) is one-to-one by A13, A14, FINSEQ_4:62;
hence Swap (E,x,y) is Enumeration of swap (F,x,y) by A13, RLAFFIN3:def 1; :: thesis: verum