defpred S₁[ object ] means ( p in loc D & $1 = ColD . p );
deffunc H₁( object ) -> Element of NAT = ((m . p) . (In ($1, the ColoredSet of CPN))) + 1;
deffunc H₂( 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
( ( S₁[x] implies H₁(x) in NAT ) & ( not S₁[x] implies H₂(x) in NAT ) ) ;
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
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(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 ) )
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) by P2;
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 ) ) ; :: thesis: verum

end;