defpred S₁[ object , object ] means ex m being Nat st
( ( $1 = IC & $2 = F₃() ) or ( $1 = intloc m & $2 = F₁(m) ) or ( $1 = fsloc m & $2 = F₂(m) ) );
A1: for e being object st e in the carrier of SCM+FSA holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis:
assume e in the carrier of SCM+FSA ; :: thesis:
then e in (Data-Locations ) \/ {(IC )} by STRUCT_0:4;
then A2: ( e in Data-Locations or e in {(IC )} ) by XBOOLE_0:def 3;

now :: thesis:

per cases by A2, SCMFSA_2:100, XBOOLE_0:def 3;

case e in {(IC )} ; :: thesis:

hence e = IC by TARSKI:def 1; :: thesis:

end;

case e in Int-Locations ; :: thesis:

then e is Int-Location by AMI_2:def 16;
hence ex m being Nat st e = intloc m by SCMFSA_2:8; :: thesis:

end;

case e in FinSeq-Locations ; :: thesis:

then e is FinSeq-Location by SCMFSA_2:def 5;
hence ex m being Nat st e = fsloc m by SCMFSA_2:9; :: thesis:

end;

end;

end;

then consider m being Nat such that
A3: ( e = IC or e = intloc m or e = fsloc m ) ;

per cases by A3;

suppose A4: e = IC ; :: thesis:

take u = F₃(); :: thesis:
thus S₁[e,u] by A4; :: thesis:

end;

suppose A5: e = intloc m ; :: thesis:

take u = F₁(m); :: thesis:
thus S₁[e,u] by A5; :: thesis:

end;

suppose A6: e = fsloc m ; :: thesis:

take u = F₂(m); :: thesis:
thus S₁[e,u] by A6; :: thesis:

end;

end;

end;

consider f being Function such that
A7: dom f = the carrier of SCM+FSA and
A8: for e being object st e in the carrier of SCM+FSA holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A9: dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def 1;

now :: thesis:

let x be object ; :: thesis:
assume A10: x in dom the Object-Kind of SCM+FSA ; :: thesis:
then consider m being Nat such that
A11: ( ( x = IC & f . x = F₃() ) or ( x = intloc m & f . x = F₁(m) ) or ( x = fsloc m & f . x = F₂(m) ) ) by A8, A9;
x in (Data-Locations ) \/ {(IC )} by A10, A9, STRUCT_0:4;
then A12: ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def 3;

per cases by A12, SCMFSA_2:100, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

then A13: x is Int-Location by AMI_2:def 16;
then (the_Values_of SCM+FSA) . x = Values (intloc m) by A11, SCMFSA_2:56, SCMFSA_2:58
.= INT by SCMFSA_2:11 ;
hence f . x in (the_Values_of SCM+FSA) . x by A11, A13, INT_1:def 2, SCMFSA_2:58; :: thesis:

end;

suppose x in FinSeq-Locations ; :: thesis:

then A14: x is FinSeq-Location by SCMFSA_2:def 5;
then (the_Values_of SCM+FSA) . x = Values (fsloc m) by A11, SCMFSA_2:57, SCMFSA_2:58
.= INT * by SCMFSA_2:12 ;
hence f . x in (the_Values_of SCM+FSA) . x by A11, A14, FINSEQ_1:def 11, SCMFSA_2:57, SCMFSA_2:58; :: thesis:

end;

suppose A15: x in {(IC )} ; :: thesis:

then A16: (the_Values_of SCM+FSA) . x = Values (IC ) by TARSKI:def 1
.= NAT by MEMSTR_0:def 6 ;
x = IC by A15, TARSKI:def 1;
hence f . x in (the_Values_of SCM+FSA) . x by A11, A16, SCMFSA_2:56, SCMFSA_2:57; :: thesis:

end;

end;

end;

then reconsider f = f as State of SCM+FSA by A7, A9, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis:
ex m being Nat st
( ( IC = IC & f . (IC ) = F₃() ) or ( IC = intloc m & f . (IC ) = F₁(m) ) or ( IC = fsloc m & f . (IC ) = F₂(m) ) ) by A8;
hence IC f = F₃() by SCMFSA_2:56, SCMFSA_2:57; :: thesis:
let i be Nat; :: thesis:
ex m being Nat st
( ( intloc i = IC & f . (intloc i) = F₃() ) or ( intloc i = intloc m & f . (intloc i) = F₁(m) ) or ( intloc i = fsloc m & f . (intloc i) = F₂(m) ) ) by A8;
hence f . (intloc i) = F₁(i) by AMI_3:10, SCMFSA_2:56, SCMFSA_2:58; :: thesis:
ex m being Nat st
( ( fsloc i = IC & f . (fsloc i) = F₃() ) or ( fsloc i = intloc m & f . (fsloc i) = F₁(m) ) or ( fsloc i = fsloc m & f . (fsloc i) = F₂(m) ) ) by A8;
hence f . (fsloc i) = F₂(i) by SCMFSA_2:57, SCMFSA_2:58; :: thesis: