let s be State of SCM+FSA ; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0 ) = 1 holds
( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )
let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0 ) = 1 holds
( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )
let f be FinSeq-Location ; :: thesis: ( 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0 ) = 1 implies ( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) ) )
set a = aa;
set b = bb;
assume that
A1: 1 <= s . aa and
A2: s . aa <= len (s . f) and
A3: 1 <= s . bb and
A4: s . bb <= len (s . f) and
A5: s . (intloc 0 ) = 1 ; :: thesis: ( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )
A6: (IExec (swap f,aa,bb),s) . f = ((s . f) +* (s . aa),((s . f) . (s . bb))) +* (s . bb),((s . f) . (s . aa)) by A1, A2, A3, A4, A5, Th39;
reconsider sa = s . aa as Element of NAT by A1, INT_1:16;
A7: sa in dom (s . f) by A1, A2, FINSEQ_3:27;
A8: dom ((s . f) +* (s . aa),((s . f) . (s . bb))) = dom (s . f) by FUNCT_7:32;
reconsider sb = s . bb as Element of NAT by A3, INT_1:16;
A9: sb in dom (s . f) by A3, A4, FINSEQ_3:27;

per cases ( sa <> sb or sa = sb ) ;

suppose sa <> sb ; :: thesis: ( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )

hence ((IExec (swap f,aa,bb),s) . f) . (s . aa) = ((s . f) +* (s . aa),((s . f) . (s . bb))) . (s . aa) by A6, FUNCT_7:34
.= (s . f) . (s . bb) by A7, FUNCT_7:33 ;
:: thesis: ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa)
thus ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) by A9, A6, A8, FUNCT_7:33; :: thesis: verum

end;

suppose sa = sb ; :: thesis: ( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )

hence ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) by A7, A6, A8, FUNCT_7:33; :: thesis: ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa)
thus ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) by A9, A6, A8, FUNCT_7:33; :: thesis: verum

end;

end;