let a, b be Int-Location ; :: thesis: for f being FinSeq-Location holds not f :=<0,...,0> b destroys a
let f be FinSeq-Location ; :: thesis: not f :=<0,...,0> b destroys a

now

let e be Int-Location ; :: thesis: for h being FinSeq-Location holds
( a := e <> f :=<0,...,0> b & AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
let h be FinSeq-Location ; :: thesis: ( a := e <> f :=<0,...,0> b & AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
A1: InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:29;
hence a := e <> f :=<0,...,0> b by SCMFSA_2:18; :: thesis: ( AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus AddTo (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:19; :: thesis: ( SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus SubFrom (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:20; :: thesis: ( MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus MultBy (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:21; :: thesis: ( Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus ( Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b ) by A1, SCMFSA_2:22; :: thesis: ( a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus a := (h,e) <> f :=<0,...,0> b by A1, SCMFSA_2:26; :: thesis: a :=len h <> f :=<0,...,0> b
thus a :=len h <> f :=<0,...,0> b by A1, SCMFSA_2:28; :: thesis: verum

end;

hence not f :=<0,...,0> b destroys a by Def3; :: thesis: verum