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

proof

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

now

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 SCMFSA_2:4;
hence ex m being Element of 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:5;
hence ex m being Element of NAT st e = fsloc m by SCMFSA_2:9; :: thesis:

end;

end;

end;

then consider m being Element of 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 A6: e = intloc m ; :: thesis:

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

end;

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

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

end;

end;

end;

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

now

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

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

suppose x in Int-Locations ; :: thesis:

then A14: x is Int-Location by SCMFSA_2:4;
then the Object-Kind of SCM+FSA . x = ObjectKind (intloc m) by A12, SCMFSA_2:56, SCMFSA_2:58
.= INT by SCMFSA_2:11 ;
hence f . x in the Object-Kind of SCM+FSA . x by A12, A14, INT_1:def 2, SCMFSA_2:58; :: thesis:

end;

suppose x in FinSeq-Locations ; :: thesis:

then A15: x is FinSeq-Location by SCMFSA_2:5;
then the Object-Kind of SCM+FSA . x = ObjectKind (fsloc m) by A12, SCMFSA_2:57, SCMFSA_2:58
.= INT * by SCMFSA_2:12 ;
hence f . x in the Object-Kind of SCM+FSA . x by A12, A15, FINSEQ_1:def 11, SCMFSA_2:57, SCMFSA_2:58; :: thesis:

end;

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

then A17: the Object-Kind of SCM+FSA . x = ObjectKind (IC ) by TARSKI:def 1
.= NAT by MEMSTR_0:def 3 ;
x = IC by A16, TARSKI:def 1;
hence f . x in the Object-Kind of SCM+FSA . x by A12, A17, SCMFSA_2:56, SCMFSA_2:57; :: thesis:

end;

end;

end;

then reconsider f = f as State of SCM+FSA by A8, A10, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis:
ex m being Element of NAT st
( ( IC = IC & f . (IC ) = F₃() ) or ( IC = intloc m & f . (IC ) = F₁(m) ) or ( IC = fsloc m & f . (IC ) = F₂(m) ) ) by A9;
hence IC f = F₃() by SCMFSA_2:56, SCMFSA_2:57; :: thesis:
let i be Element of NAT ; :: thesis:
ex m being Element of 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 A9;
hence f . (intloc i) = F₁(i) by AMI_3:10, SCMFSA_2:56, SCMFSA_2:58; :: thesis:
ex m being Element of 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 A9;
hence f . (fsloc i) = F₂(i) by SCMFSA_2:57, SCMFSA_2:58; :: thesis: