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
A5: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) and
A6: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ; :: thesis: M1 = M2
let p be object ; :: according to PNPROC_1:def 1 :: thesis: ( p in P implies p multitude_of = p multitude_of )
assume A7: p in P ; :: thesis: p multitude_of = p multitude_of
hence p multitude_of = (p multitude_of ) - (p multitude_of ) by A5
.= p multitude_of by A6, A7 ;
:: thesis: verum