let s1, s2 be State of SCM+FSA; :: thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int-Location holds s1 . a = s2 . a and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: s1 = s2
s1 in product (SCM*-VAL * SCM+FSA-OK) by CARD_3:107;
then consider g1 being Function such that
A4: s1 = g1 and
A5: dom g1 = dom (SCM*-VAL * SCM+FSA-OK) and
for x being object st x in dom (SCM*-VAL * SCM+FSA-OK) holds
g1 . x in (SCM*-VAL * SCM+FSA-OK) . x by CARD_3:def 5;
s2 in product (SCM*-VAL * SCM+FSA-OK) by CARD_3:107;
then consider g2 being Function such that
A6: s2 = g2 and
A7: dom g2 = dom (SCM*-VAL * SCM+FSA-OK) and
for x being object st x in dom (SCM*-VAL * SCM+FSA-OK) holds
g2 . x in (SCM*-VAL * SCM+FSA-OK) . x by CARD_3:def 5;

A8: now :: thesis: for x being object st x in SCM+FSA-Memory holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in SCM+FSA-Memory implies g1 . b₁ = g2 . b₁ )
assume x in SCM+FSA-Memory ; :: thesis: g1 . b₁ = g2 . b₁
then x in ({(IC )} \/ SCM-Data-Loc) \/ SCM+FSA-Data*-Loc by Th1;
then A9: ( x in {(IC )} \/ SCM-Data-Loc or x in SCM+FSA-Data*-Loc ) by XBOOLE_0:def 3;
A10: Int-Locations = SCM+FSA-Data-Loc ;

per cases ( x in {(IC )} or x in SCM-Data-Loc or x in SCM+FSA-Data*-Loc ) by A9, XBOOLE_0:def 3;

suppose x in {(IC )} ; :: thesis: g1 . b₁ = g2 . b₁

then x = IC by TARSKI:def 1;
hence g1 . x = g2 . x by A1, A4, A6; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: g1 . b₁ = g2 . b₁

then x is Int-Location by A10, AMI_2:def 16;
hence g1 . x = g2 . x by A2, A4, A6; :: thesis: verum

end;

suppose x in SCM+FSA-Data*-Loc ; :: thesis: g1 . b₁ = g2 . b₁

then x is FinSeq-Location by Def3;
hence g1 . x = g2 . x by A3, A4, A6; :: thesis: verum

end;

end;

end;

thus s1 = s2 by A4, A5, A6, A7, A8; :: thesis: verum