defpred S_{1}[ object ] means ( p in loc D & $1 = ColD . p );

deffunc H_{1}( object ) -> set = ((m . p) . (In ($1, the ColoredSet of CPN))) - 1;

deffunc H_{2}( 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_{1}[x] implies H_{1}(x) in NAT ) & ( not S_{1}[x] implies H_{2}(x) in NAT ) )

P2: for x being object st x in the ColoredSet of CPN holds

( ( S_{1}[x] implies f . x = H_{1}(x) ) & ( not S_{1}[x] implies f . x = H_{2}(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

deffunc H

deffunc H

P1: for x being object st x in the ColoredSet of CPN holds

( ( S

proof

consider f being Function of the ColoredSet of CPN,NAT such that
let x be object ; :: thesis: ( x in the ColoredSet of CPN implies ( ( S_{1}[x] implies H_{1}(x) in NAT ) & ( not S_{1}[x] implies H_{2}(x) in NAT ) ) )

assume P10: x in the ColoredSet of CPN ; :: thesis: ( ( S_{1}[x] implies H_{1}(x) in NAT ) & ( not S_{1}[x] implies H_{2}(x) in NAT ) )

( S_{1}[x] implies H_{1}(x) in NAT )
_{1}[x] implies H_{1}(x) in NAT ) & ( not S_{1}[x] implies H_{2}(x) in NAT ) )
; :: thesis: verum

end;assume P10: x in the ColoredSet of CPN ; :: thesis: ( ( S

( S

proof

hence
( ( S
assume p:
S_{1}[x]
; :: thesis: H_{1}(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 H_{1}(x) in NAT
by INT_1:3; :: thesis: verum

end;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 H

P2: for x being object st x in the ColoredSet of CPN holds

( ( S

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;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