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

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