set S1 = {(IC )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
defpred S₁[ set , set ] means ex m being Element of NAT st
( ( $1 = IC & $2 = F₂() ) or ( $1 = DataLoc (m,0) & $2 = F₁(m) ) );
A1: for e being set st e in the carrier of SCMPDS holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in the carrier of SCMPDS implies ex u being set st S₁[e,u] )
assume e in the carrier of SCMPDS ; :: thesis: ex u being set st S₁[e,u]
then e in {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then A2: e in {(IC )} \/ SCM-Data-Loc ;

now

per cases ( e in {(IC )} or e in SCM-Data-Loc ) by A2, XBOOLE_0:def 3;

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

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

end;

case e in SCM-Data-Loc ; :: thesis: ex m being Element of NAT st e = DataLoc (m,0)

then e is Int_position by SCMPDS_2:3;
hence ex m being Element of NAT st e = DataLoc (m,0) by Th18; :: thesis: verum

end;

end;

end;

then consider m being Element of NAT such that
A3: ( e = IC or e = DataLoc (m,0) ) ;

per cases ( e = IC or e = DataLoc (m,0) ) by A3;

suppose A4: e = IC ; :: thesis: ex u being set st S₁[e,u]

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

end;

suppose A6: e = DataLoc (m,0) ; :: thesis: ex u being set st S₁[e,u]

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

end;

end;

end;

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

now

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies f . b₁ in the Object-Kind of SCMPDS . b₁ )
assume A10: x in dom the Object-Kind of SCMPDS ; :: thesis: f . b₁ in the Object-Kind of SCMPDS . b₁
then x in {(IC )} \/ SCM-Data-Loc by A9, SCMPDS_2:84, STRUCT_0:4;
then A11: x in {(IC )} \/ SCM-Data-Loc ;
consider m being Element of NAT such that
A12: ( ( x = IC & f . x = F₂() ) or ( x = DataLoc (m,0) & f . x = F₁(m) ) ) by A8, A9, A10;

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

suppose x in SCM-Data-Loc ; :: thesis: f . b₁ in the Object-Kind of SCMPDS . b₁

then x is Int_position by SCMPDS_2:3;
then the Object-Kind of SCMPDS . x = ObjectKind (DataLoc (m,0)) by A12, SCMPDS_2:43
.= INT by SCMPDS_2:5 ;
hence f . x in the Object-Kind of SCMPDS . x by A12, INT_1:def 2; :: thesis: verum

end;

suppose A14: x in {(IC )} ; :: thesis: f . b₁ in the Object-Kind of SCMPDS . b₁

then the Object-Kind of SCMPDS . x = ObjectKind (IC ) by TARSKI:def 1
.= NAT by MEMSTR_0:def 3 ;
hence f . x in the Object-Kind of SCMPDS . x by A12, A14, SCMPDS_2:2, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then reconsider f = f as State of SCMPDS by A7, A9, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
consider m being Element of NAT such that
A15: ( ( IC = IC & f . (IC ) = F₂() ) or ( IC = DataLoc (m,0) & f . (IC ) = F₁(m) ) ) by A8;
take f ; :: thesis: ( IC f = F₂() & ( for i being Element of NAT holds f . (DataLoc (i,0)) = F₁(i) ) )
thus IC f = F₂() by A15, SCMPDS_2:43; :: thesis: for i being Element of NAT holds f . (DataLoc (i,0)) = F₁(i)
let i be Element of NAT ; :: thesis: f . (DataLoc (i,0)) = F₁(i)
ex m being Element of NAT st
( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F₂() ) or ( DataLoc (i,0) = DataLoc (m,0) & f . (DataLoc (i,0)) = F₁(m) ) ) by A8;
hence f . (DataLoc (i,0)) = F₁(i) by Th17, SCMPDS_2:43; :: thesis: verum