let P be set ; :: thesis: for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)
let m1, m2, m3 be marking of P; :: thesis: (m1 + m2) + m3 = m1 + (m2 + m3)
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
then A2: ((m1 + m2) + m3) . p = ((m1 + m2) . p) + (m3 . p) by Def4
.= ((m1 . p) + (m2 . p)) + (m3 . p) by A1, Def4 ;
(m1 + (m2 + m3)) . p = (m1 . p) + ((m2 + m3) . p) by A1, Def4
.= (m1 . p) + ((m2 . p) + (m3 . p)) by A1, Def4
.= ((m1 . p) + (m2 . p)) + (m3 . p) ;
hence p multitude_of = p multitude_of by A2; :: thesis: verum