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_{1}[ 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 ) );

A4: for s being Element of product (the_Values_of SCMPDS) holds S_{1}[s,f . s]
from FUNCT_2:sch 3(A1);

A5: for s being State of SCMPDS holds S_{1}[s,f . s]

( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )

for s being State of SCMPDS holds

( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )

defpred S

( 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_{1}[s,y]

consider f being Function of (product (the_Values_of SCMPDS)),NAT such that let s be Element of product (the_Values_of SCMPDS); :: thesis: ex y being Element of NAT st S_{1}[y,b_{2}]

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

end;

suppose A2:
s . a <= 0
; :: thesis: ex y being Element of NAT st S_{1}[y,b_{2}]

reconsider y = 0 as Element of NAT ;

take y = y; :: thesis: S_{1}[s,y]

thus S_{1}[s,y]
by A2; :: thesis: verum

end;take y = y; :: thesis: S

thus S

suppose A3:
s . a > 0
; :: thesis: ex y being Element of NAT st S_{1}[y,b_{2}]

then reconsider y = s . a as Element of NAT by INT_1:3;

take y = y; :: thesis: S_{1}[s,y]

thus S_{1}[s,y]
by A3; :: thesis: verum

end;take y = y; :: thesis: S

thus S

A4: for s being Element of product (the_Values_of SCMPDS) holds S

A5: for s being State of SCMPDS holds S

proof

take
f
; :: thesis: for s being State of SCMPDS holds
let s be State of SCMPDS; :: thesis: S_{1}[s,f . s]

reconsider s = s as Element of product (the_Values_of SCMPDS) by CARD_3:107;

S_{1}[s,f . s]
by A4;

hence S_{1}[s,f . s]
; :: thesis: verum

end;reconsider s = s as Element of product (the_Values_of SCMPDS) by CARD_3:107;

S

hence S

( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )