let a, b, c be Int-Location ; :: thesis: for f being FinSeq-Location holds not (f,c) := b destroys a
let f be FinSeq-Location ; :: thesis: not (f,c) := b destroys a

now

let e be Int-Location ; :: thesis: for h being FinSeq-Location holds
( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
let h be FinSeq-Location ; :: thesis: ( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
A1: InsCode ((f,c) := b) = 10 by SCMFSA_2:51;
hence a := e <> (f,c) := b by SCMFSA_2:42; :: thesis: ( AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
thus AddTo (a,e) <> (f,c) := b by A1, SCMFSA_2:43; :: thesis: ( SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
thus SubFrom (a,e) <> (f,c) := b by A1, SCMFSA_2:44; :: thesis: ( MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
thus MultBy (a,e) <> (f,c) := b by A1, SCMFSA_2:45; :: thesis: ( Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
thus ( Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b ) by A1, SCMFSA_2:46; :: thesis: ( a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )
thus a := (h,e) <> (f,c) := b by A1, SCMFSA_2:50; :: thesis: a :=len h <> (f,c) := b
thus a :=len h <> (f,c) := b by A1, SCMFSA_2:52; :: thesis: verum

end;

hence not (f,c) := b destroys a by Def3; :: thesis: verum