defpred S1[ object ] means ( p in loc D & $1 = ColD . p );
deffunc H1( object ) -> set = ((m . p) . (In ($1, the ColoredSet of CPN))) - 1;
deffunc H2( object ) -> Element of NAT = (m . p) . (In ($1, the ColoredSet of CPN));
P1: for x being object st x in the ColoredSet of CPN holds
( ( S1[x] implies H1(x) in NAT ) & ( not S1[x] implies H2(x) in NAT ) )
proof
let x be object ; :: thesis: ( x in the ColoredSet of CPN implies ( ( S1[x] implies H1(x) in NAT ) & ( not S1[x] implies H2(x) in NAT ) ) )
assume P10: x in the ColoredSet of CPN ; :: thesis: ( ( S1[x] implies H1(x) in NAT ) & ( not S1[x] implies H2(x) in NAT ) )
( S1[x] implies H1(x) in NAT )
proof
assume p: S1[x] ; :: thesis: H1(x) in NAT
x = In (x, the ColoredSet of CPN) by P10, SUBSET_1:def 8;
then 1 - 1 <= ((m . p) . (In (x, the ColoredSet of CPN))) - 1 by AS1, p, XREAL_1:9;
hence H1(x) in NAT by INT_1:3; :: thesis: verum
end;
hence ( ( S1[x] implies H1(x) in NAT ) & ( not S1[x] implies H2(x) in NAT ) ) ; :: thesis: verum
end;
consider f being Function of the ColoredSet of CPN,NAT such that
P2: for x being object st x in the ColoredSet of CPN holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch 5(P1);
 take f ; :: thesis: for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies f . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f . x = (m . p) . x ) )
thus for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies f . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f . x = (m . p) . x ) ) :: thesis: verum
proof
let x be Element of the ColoredSet of CPN; :: thesis: ( ( p in loc D & x = ColD . p implies f . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f . x = (m . p) . x ) )
x = In (x, the ColoredSet of CPN) ;
hence ( ( p in loc D & x = ColD . p implies f . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f . x = (m . p) . x ) ) by P2; :: thesis: verum
end;