hereby :: thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b₁ being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b₁ = {f} ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b₁ being Element of Fin FinSeq-Locations st b₁ = {} ) )

assume ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis: ex IT being Element of Fin FinSeq-Locations ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} )
then consider a, b being Int-Location, f being FinSeq-Location such that
A1: ( i = b := (f,a) or i = (f,a) := b ) by SCMFSA_2:38, SCMFSA_2:39;
reconsider f9 = f as Element of FinSeq-Locations by SCMFSA_2:def 5;
reconsider IT = {.f9.} as Element of Fin FinSeq-Locations ;
take IT = IT; :: thesis: ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} )
take a = a; :: thesis: ex b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} )
take b = b; :: thesis: ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} )
take f = f; :: thesis: ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} )
thus ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) by A1; :: thesis: verum

end;

hereby :: thesis: ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b₁ being Element of Fin FinSeq-Locations st b₁ = {} )

assume ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis: ex IT being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} )
then consider a being Int-Location, f being FinSeq-Location such that
A2: ( i = a :=len f or i = f :=<0,...,0> a ) by SCMFSA_2:40, SCMFSA_2:41;
reconsider f9 = f as Element of FinSeq-Locations by SCMFSA_2:def 5;
reconsider IT = {.f9.} as Element of Fin FinSeq-Locations ;
take IT = IT; :: thesis: ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} )
take a = a; :: thesis: ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} )
take f = f; :: thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} )
thus ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) by A2; :: thesis: verum

end;

{} in Fin FinSeq-Locations by FINSUB_1:7;
hence ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b₁ being Element of Fin FinSeq-Locations st b₁ = {} ) ; :: thesis: verum