let a, b, c be Int-Location ; :: thesis: ( a <> b implies not AddTo (b,c) destroys a )
assume A1: a <> b ; :: thesis: not AddTo (b,c) destroys a

now

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

end;

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