let f1, f2 be Function of the ColoredSet of CPN,NAT; :: thesis: ( ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies f1 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f1 . x = (m . p) . x ) ) ) & ( for x being Element of the ColoredSet of CPN holds
( ( p in loc D & x = ColD . p implies f2 . x = ((m . p) . x) + 1 ) & ( ( not p in loc 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 in loc D & x = ColD . p implies f1 . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies f1 . x = (m . p) . x ) ) ; :: thesis: ( ex x being Element of the ColoredSet of CPN st
( ( p in loc D & x = ColD . p implies f2 . x = ((m . p) . x) + 1 ) implies ( ( not p in loc 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 in loc D & x = ColD . p implies f2 . x = ((m . p) . x) + 1 ) & ( ( not p in loc 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
proof
let x be Element of the ColoredSet of CPN; :: thesis: f1 . x = f2 . x
per cases ( ( p in loc D & x = ColD . p ) or not p in loc D or not x = ColD . p ) ;
suppose P1: ( p in loc D & x = ColD . p ) ; :: thesis: f1 . x = f2 . x
hence f1 . x = ((m . p) . x) + 1 by A1
.= f2 . x by A2, P1 ;
:: thesis: verum
end;
suppose P2: ( not p in loc D or not x = ColD . p ) ; :: thesis: f1 . x = f2 . x
hence f1 . x = (m . p) . x by A1
.= f2 . x by A2, P2 ;
:: thesis: verum
end;
end;
end;
hence f1 = f2 by FUNCT_2:def 7; :: thesis: verum