let a, b 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 = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max (abs (s . a)),(abs (s . b)) ) )
defpred S₁[ set , set ] means ex t being State of SCMPDS st
( t = $1 & ( t . a = t . b implies $2 = 0 ) & ( t . a <> t . b implies $2 = max (abs (t . a)),(abs (t . b)) ) );

A1: now

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

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

suppose A2: s . a = s . b ; :: 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 <> s . b ; :: thesis: ex y being Element of NAT st S₁[y,b₂]

set mm = max (abs (s . a)),(abs (s . b));
reconsider y = max (abs (s . a)),(abs (s . b)) as Element of NAT by XXREAL_0: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 = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max (abs (s . a)),(abs (s . b)) ) )

hereby :: thesis: verum

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

end;