let x, y, z be object ; :: thesis: for f being Function st z in dom f holds
Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*>
let f be Function; :: thesis: ( z in dom f implies Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*> )
assume A1: z in dom f ; :: thesis: Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*>
A2: 1 in Seg 1 ;
A3: ( dom (Swap (<*(f . z)*>,x,y)) = dom <*(f . z)*> & dom <*(f . z)*> = Seg 1 ) by Def4, FINSEQ_1:38;
then A4: ( len (Swap (<*(f . z)*>,x,y)) = len <*(f . z)*> & len <*(f . z)*> = 1 ) by FINSEQ_3:29, FINSEQ_1:40;
A5: <*(f . z)*> . 1 = f . z ;

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

suppose x in f . z ; :: thesis: Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*>

then ( (Swap (<*(f . z)*>,x,y)) . 1 = ((f . z) \ {x}) \/ {y} & ((f . z) \ {x}) \/ {y} = (Swap (f,x,y)) . z ) by A2, Def4, A3, A5, A1;
hence Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*> by A4, FINSEQ_1:40; :: thesis: verum

end;

suppose not x in f . z ; :: thesis: Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*>

then ( (Swap (<*(f . z)*>,x,y)) . 1 = (f . z) \/ {x} & (f . z) \/ {x} = (Swap (f,x,y)) . z ) by A2, Def4, A3, A5, A1;
hence Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*> by A4, FINSEQ_1:40; :: thesis: verum

end;

end;