let f1, f2 be Function of the ColoredSet of CPN,NAT; :: thesis: ( ( for x being Element of the ColoredSet of CPN holds ( ( p inloc D & x = ColD . p implies f1 . x =((m . p). x)- 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f1 . x =(m . p). x ) ) ) & ( for x being Element of the ColoredSet of CPN holds ( ( p inloc D & x = ColD . p implies f2 . x =((m . p). x)- 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f2 . x =(m . p). x ) ) ) implies f1 = f2 ) assume A1:
for x being Element of the ColoredSet of CPN holds ( ( p inloc D & x = ColD . p implies f1 . x =((m . p). x)- 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f1 . x =(m . p). x ) )
; :: thesis: ( ex x being Element of the ColoredSet of CPN st ( ( p inloc D & x = ColD . p implies f2 . x =((m . p). x)- 1 ) implies ( ( not p inloc D or not x = ColD . p ) & not f2 . x =(m . p). x ) ) or f1 = f2 ) assume A2:
for x being Element of the ColoredSet of CPN holds ( ( p inloc D & x = ColD . p implies f2 . x =((m . p). x)- 1 ) & ( ( not p inloc D or not x = ColD . p ) implies f2 . x =(m . p). x ) )
; :: thesis: f1 = f2
for x being Element of the ColoredSet of CPN holds f1 . x = f2 . x