let a be Int_position; :: thesis: ex f being Function of (product (the_Values_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 :: thesis: for s being Element of product (the_Values_of SCMPDS) ex y being Element of NAT st S₁[s,y]

let s be Element of product (the_Values_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:58;
then reconsider y = - (s . a) as Element of NAT by INT_1:3;
take y = y; :: thesis: S₁[s,y]
thus S₁[s,y] by A3; :: thesis: verum

end;

end;

end;

consider f being Function of (product (the_Values_of SCMPDS)),NAT such that
A4: for s being Element of product (the_Values_of SCMPDS) holds S₁[s,f . s] from FUNCT_2:sch 3(A1);
A5: for s being State of SCMPDS holds S₁[s,f . s]

proof

let s be State of SCMPDS; :: thesis: S₁[s,f . s]
reconsider s = s as Element of product (the_Values_of SCMPDS) by CARD_3:107;
S₁[s,f . s] by A4;
hence S₁[s,f . s] ; :: thesis: verum

end;

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 A5;
hence ( ( s . a >= 0 implies f . s = 0 ) & ( s . a < 0 implies f . s = - (s . a) ) ) ; :: thesis: verum

end;