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

proof

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

now :: thesis: ( ( e in {(IC )} & e = IC ) or ( e in SCM-Data-Loc & ex m being Nat st e = DataLoc (m,0) ) )

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 Nat st e = DataLoc (m,0)

then e is Int_position by AMI_2:def 16;
hence ex m being Nat st e = DataLoc (m,0) by Th4; :: thesis: verum

end;

end;

end;

then consider m being 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 object st S₁[e,u]

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

end;

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

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

end;

end;

end;

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

now :: thesis: for x being object st x in dom the Object-Kind of SCMPDS holds
f . x in (the_Values_of SCMPDS) . x

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

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

suppose x in SCM-Data-Loc ; :: thesis: f . b₁ in (the_Values_of SCMPDS) . b₁

then x is Int_position by AMI_2:def 16;
then (the_Values_of SCMPDS) . x = Values (DataLoc (m,0)) by A11, SCMPDS_2:43
.= INT by SCMPDS_2:5 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, INT_1:def 2; :: thesis: verum

end;

suppose A12: x in {(IC )} ; :: thesis: f . b₁ in (the_Values_of SCMPDS) . b₁

(the_Values_of SCMPDS) . x = Values (IC ) by TARSKI:def 1, A12
.= NAT by MEMSTR_0:def 6 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, A12, SCMPDS_2:2, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then reconsider f = f as State of SCMPDS by A6, A8, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
consider m being Nat such that
A13: ( ( IC = IC & f . (IC ) = F₂() ) or ( IC = DataLoc (m,0) & f . (IC ) = F₁(m) ) ) by A7;
take f ; :: thesis: ( IC f = F₂() & ( for i being Nat holds f . (DataLoc (i,0)) = F₁(i) ) )
thus IC f = F₂() by A13, SCMPDS_2:43; :: thesis: for i being Nat holds f . (DataLoc (i,0)) = F₁(i)
let i be Nat; :: thesis: f . (DataLoc (i,0)) = F₁(i)
ex m being 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 A7;
hence f . (DataLoc (i,0)) = F₁(i) by Th3, SCMPDS_2:43; :: thesis: verum