defpred S₁[ set , set ] means ex m being Element of NAT st
( ( $1 = IC SCM+FSA & $2 = F₄() ) or ( $1 = m & $2 = F₁(m) ) 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]

let e be set ; :: thesis:
assume e in the carrier of SCM+FSA ; :: thesis:
then ( e in (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} or e in NAT ) by SCMFSA_2:8, XBOOLE_0:def 3;
then A2: ( e in Int-Locations \/ FinSeq-Locations or e in {(IC SCM+FSA)} or e in NAT ) by XBOOLE_0:def 3;

per cases by A2, XBOOLE_0:def 3;

case e in {(IC SCM+FSA)} ; :: thesis:

hence e = IC SCM+FSA by TARSKI:def 1; :: thesis:

end;

case e in Int-Locations ; :: thesis:

then e is Int-Location by SCMFSA_2:11;
hence ex m being Element of NAT st e = intloc m by SCMFSA_2:19; :: thesis:

end;

case e in FinSeq-Locations ; :: thesis:

then e is FinSeq-Location by SCMFSA_2:12;
hence ex m being Element of NAT st e = fsloc m by SCMFSA_2:20; :: thesis:

end;

case e in NAT ; :: thesis:

then reconsider l = e as Element of NAT ;
reconsider m = l as Element of NAT ;
take m = m; :: thesis:
thus e = m ; :: thesis:

end;

end;

end;

then consider m being Element of NAT such that
A3: ( e = IC SCM+FSA or e = m or e = intloc m or e = fsloc m ) ;

per cases by A3;

suppose A4: e = IC SCM+FSA ; :: thesis:

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

end;

suppose A5: e = m ; :: thesis:

take u = F₁(m); :: thesis:
thus S₁[e,u] by A5; :: 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;

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 SCM+FSA & f . x = F₄() ) or ( x = m & f . x = F₁(m) ) or ( x = intloc m & f . x = F₂(m) ) or ( x = fsloc m & f . x = F₃(m) ) ) by A9, A10;
( x in (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} or x in NAT ) by A10, A11, SCMFSA_2:8, XBOOLE_0:def 3;
then A13: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA)} or x in NAT ) by XBOOLE_0:def 3;

per cases by A13, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

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

end;

suppose x in FinSeq-Locations ; :: thesis:

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

end;

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

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

end;

suppose x in NAT ; :: thesis:

then reconsider l = x as Element of NAT ;
the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by COMPOS_1:def 8;
hence f . x in the Object-Kind of SCM+FSA . x by A12, COMPOS_1:3, SCMFSA_2:84, SCMFSA_2:85; :: thesis:

end;

end;

end;

then reconsider f = f as State of SCM+FSA by A8, A10, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
take f ; :: thesis:
ex m being Element of NAT st
( ( IC SCM+FSA = IC SCM+FSA & f . (IC SCM+FSA) = F₄() ) or ( IC SCM+FSA = m & f . (IC SCM+FSA) = F₁(m) ) or ( IC SCM+FSA = intloc m & f . (IC SCM+FSA) = F₂(m) ) or ( IC SCM+FSA = fsloc m & f . (IC SCM+FSA) = F₃(m) ) ) by A9;
hence IC f = F₄() by COMPOS_1:3, SCMFSA_2:81, SCMFSA_2:82; :: thesis:
let i be Element of NAT ; :: thesis:
X: i in NAT ;
ex m being Element of NAT st
( ( i = IC SCM+FSA & f . i = F₄() ) or ( i = m & f . i = F₁(m) ) or ( i = intloc m & f . i = F₂(m) ) or ( i = fsloc m & f . i = F₃(m) ) ) by X, A9;
hence f . i = F₁(i) by COMPOS_1:3, SCMFSA_2:84, SCMFSA_2:85; :: thesis:
ex m being Element of NAT st
( ( intloc i = IC SCM+FSA & f . (intloc i) = F₄() ) or ( intloc i = m & f . (intloc i) = F₁(m) ) 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:52, SCMFSA_2:81, SCMFSA_2:83, SCMFSA_2:84; :: thesis:
ex m being Element of NAT st
( ( fsloc i = IC SCM+FSA & f . (fsloc i) = F₄() ) or ( fsloc i = m & f . (fsloc i) = F₁(m) ) 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:82, SCMFSA_2:83, SCMFSA_2:85; :: thesis: