let P be set ; :: thesis: for m1, m2 being marking of P holds (m1 + m2) - m2 = m1
let m1, m2 be marking of P; :: thesis: (m1 + m2) - m2 = m1
let p be object ; :: according to PNPROC_1:def 1 :: thesis: ( p in P implies p multitude_of = p multitude_of )
assume A1: p in P ; :: thesis: p multitude_of = p multitude_of
m2 c= m1 + m2 by Th4;
hence ((m1 + m2) - m2) . p = ((m1 + m2) . p) - (m2 . p) by A1, Def5
.= ((m1 . p) + (m2 . p)) - (m2 . p) by A1, Def4
.= m1 . p ;
:: thesis: verum