let a, b, c be Int-Location; for f being FinSeq-Location st a <> b holds
not b := (f,c) destroys a
let f be FinSeq-Location ; ( a <> b implies not b := (f,c) destroys a )
assume A1:
a <> b
; not b := (f,c) destroys a
now for e being Int-Location
for l being Element of NAT
for h being FinSeq-Location holds
( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )let e be
Int-Location;
for l being Element of NAT
for h being FinSeq-Location holds
( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )let l be
Element of
NAT ;
for h being FinSeq-Location holds
( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )let h be
FinSeq-Location ;
( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )A2:
InsCode (b := (f,c)) = 9
by SCMFSA_2:26;
hence
a := e <> b := (
f,
c)
by SCMFSA_2:18;
( AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )thus
AddTo (
a,
e)
<> b := (
f,
c)
by A2, SCMFSA_2:19;
( SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )thus
SubFrom (
a,
e)
<> b := (
f,
c)
by A2, SCMFSA_2:20;
( MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )thus
MultBy (
a,
e)
<> b := (
f,
c)
by A2, SCMFSA_2:21;
( Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )thus
(
Divide (
a,
e)
<> b := (
f,
c) &
Divide (
e,
a)
<> b := (
f,
c) )
by A2, SCMFSA_2:22;
( a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) )thus
a := (
h,
e)
<> b := (
f,
c)
by A1, SF_MASTR:9;
a :=len h <> b := (f,c)thus
a :=len h <> b := (
f,
c)
by A2, SCMFSA_2:28;
verum end;
hence
not b := (f,c) destroys a
; verum