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

now :: thesis: for c being Int-Location
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 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:28;
hence a := c <> b :=len f by SCMFSA_2:18; :: 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:19; :: 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:20; :: 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:21; :: 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:22; :: thesis: ( a := (g,c) <> b :=len f & a :=len g <> b :=len f )
thus a := (g,c) <> b :=len f by A2, SCMFSA_2:26; :: thesis: a :=len g <> b :=len f
thus a :=len g <> b :=len f by A1, SF_MASTR:11; :: thesis: verum

end;

hence not b :=len f destroys a ; :: thesis: verum