let M1, M2 be marking of P; :: thesis: ( ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) implies M1 = M2 )
assume that
A4: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) and
A5: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ; :: thesis: M1 = M2
let p be set ; :: according to PNPROC_1:def 1 :: thesis: ( p in P implies p multitude_of = p multitude_of )
assume A6: p in P ; :: thesis: p multitude_of = p multitude_of
hence p multitude_of = (p multitude_of ) - (p multitude_of ) by A4
.= p multitude_of by A5, A6 ;
:: thesis: verum