let a, b 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 = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max (|.(s . a).|,|.(s . b).|) ) )
defpred S1[ 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 (|.(t . a).|,|.(t . b).|) ) );
A1: now :: thesis: for s being Element of product (the_Values_of SCMPDS) ex y being Element of NAT st S1[s,y]
let s be Element of product (the_Values_of SCMPDS); :: thesis: ex y being Element of NAT st S1[y,b2]
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 S1[y,b2]
reconsider y = 0 as Element of NAT ;
take y = y; :: thesis: S1[s,y]
thus S1[s,y] by A2; :: thesis: verum
end;
suppose A3: s . a <> s . b ; :: thesis: ex y being Element of NAT st S1[y,b2]
set mm = max (|.(s . a).|,|.(s . b).|);
reconsider y = max (|.(s . a).|,|.(s . b).|) as Element of NAT by XXREAL_0:16;
take y = y; :: thesis: S1[s,y]
thus S1[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 S1[s,f . s] from FUNCT_2:sch 3(A1);
 A5: for s being State of SCMPDS holds S1[s,f . s]
proof
let s be State of SCMPDS; :: thesis: S1[s,f . s]
reconsider s = s as Element of product (the_Values_of SCMPDS) by CARD_3:107;
S1[s,f . s] by A4;
hence S1[s,f . s] ; :: thesis: verum
end;
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 (|.(s . a).|,|.(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 (|.(s . a).|,|.(s . b).|) ) )
S1[s,f . s] by A5;
hence ( ( s . a = s . b implies f . s = 0 ) & ( s . a <> s . b implies f . s = max (|.(s . a).|,|.(s . b).|) ) ) ; :: thesis: verum
end;