let a, b be Int-Location ; :: thesis: for f being FinSeq-Location st a <> b holds
not b :=len f destroysdestroy a
let f be FinSeq-Location ; :: thesis: ( a <> b implies not b :=len f destroysdestroy a )
assume A1: a <> b ; :: thesis: not b :=len f destroysdestroy a

now

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

end;

hence not b :=len f destroysdestroy a by Def3; :: thesis: verum