let a, b, x, y be object ; :: thesis: for f being Function st b <> x & b <> y holds
( b in (Swap (f,x,y)) . a iff b in f . a )
let f be Function; :: thesis: ( b <> x & b <> y implies ( b in (Swap (f,x,y)) . a iff b in f . a ) )
assume A1: ( b <> x & b <> y ) ; :: thesis: ( b in (Swap (f,x,y)) . a iff b in f . a )
thus ( b in (Swap (f,x,y)) . a implies b in f . a ) :: thesis: ( b in f . a implies b in (Swap (f,x,y)) . a )

proof

assume A2: b in (Swap (f,x,y)) . a ; :: thesis: b in f . a
then a in dom (Swap (f,x,y)) by FUNCT_1:def 2;
then A3: a in dom f by Def4;

per cases ( x in f . a or not x in f . a ) ;

suppose x in f . a ; :: thesis: b in f . a

then (Swap (f,x,y)) . a = ((f . a) \ {x}) \/ {y} by Def4, A3;
then b in (f . a) \ {x} by A2, A1, ZFMISC_1:136;
hence b in f . a ; :: thesis: verum

end;

suppose not x in f . a ; :: thesis: b in f . a

then (Swap (f,x,y)) . a = (f . a) \/ {x} by A3, Def4;
hence b in f . a by A2, A1, ZFMISC_1:136; :: thesis: verum

end;

end;

end;

assume A4: b in f . a ; :: thesis: b in (Swap (f,x,y)) . a
then A5: a in dom f by FUNCT_1:def 2;
b in (f . a) \ {x} by ZFMISC_1:56, A4, A1;
then A6: b in ((f . a) \ {x}) \/ {y} by XBOOLE_0:def 3;

per cases ( x in f . a or not x in f . a ) ;

suppose x in f . a ; :: thesis: b in (Swap (f,x,y)) . a

hence b in (Swap (f,x,y)) . a by A6, Def4, A5; :: thesis: verum

end;

suppose not x in f . a ; :: thesis: b in (Swap (f,x,y)) . a

then (Swap (f,x,y)) . a = (f . a) \/ {x} by A5, Def4;
hence b in (Swap (f,x,y)) . a by A4, ZFMISC_1:136; :: thesis: verum

end;

end;