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 Element of product the Object-Kind 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 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;

consider f being Function of (product the Object-Kind of SCMPDS ),NAT such that
B4: for s being Element of product the Object-Kind of SCMPDS holds S₁[s,f . s] from FUNCT_2:sch 3(A1);
A4: 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 Object-Kind of SCMPDS by PBOOLE:155;
S₁[s,f . s] by B4;
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 A4;
hence ( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) ) ; :: thesis: verum

end;