let a be Int_position ; :: thesis: ex f being Function of (product the Object-Kind of SCMPDS ),NAT st
for s being State of SCMPDS holds
( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) )
defpred S₁[ set , set ] means ex t being State of SCMPDS st
( t = $1 & ( t . a >= 0 implies $2 = 0 ) & ( t . a < 0 implies $2 = - (t . a) ) );

A1: now

let s be State of SCMPDS ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

per cases ( s . a >= 0 or s . a < 0 ) ;

suppose A2: s . a >= 0 ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

reconsider y = 0 as Element of NAT ;
take y = y; :: thesis: S₁[s,y]
thus S₁[s,y] by A2; :: thesis: verum

end;

suppose A3: s . a < 0 ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

then - (s . a) > 0 by XREAL_1:60;
then reconsider y = - (s . a) as Element of NAT by INT_1:16;
take y = y; :: thesis: S₁[s,y]
thus S₁[s,y] by A3; :: thesis: verum

end;

end;

end;

ex f being Function of (product the Object-Kind of SCMPDS ),NAT st
for s being State of SCMPDS holds S₁[s,f . s] from FUNCT_2:sch 3(A1);
then consider f being Function of (product the Object-Kind of SCMPDS ),NAT such that
A4: for s being State of SCMPDS holds S₁[s,f . s] ;
take f ; :: thesis: for s being State of SCMPDS holds
( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) )

hereby :: thesis: verum

let s be State of SCMPDS ; :: thesis: ( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) )
S₁[s,f . s] by A4;
hence ( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) ) ; :: thesis: verum

end;