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