deffunc H_{1}( set ) -> Element of NAT = ($1 multitude_of ) -' ($1 multitude_of );

consider m being marking of P such that

A2: for p being set st p in P holds

p multitude_of = H_{1}(p)
from PNPROC_1:sch 1();

take m ; :: thesis: for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of )

let p be set ; :: thesis: ( p in P implies p multitude_of = (p multitude_of ) - (p multitude_of ) )

assume A3: p in P ; :: thesis: p multitude_of = (p multitude_of ) - (p multitude_of )

then A4: p multitude_of >= p multitude_of by A1;

thus p multitude_of = (p multitude_of ) -' (p multitude_of ) by A2, A3

.= (p multitude_of ) - (p multitude_of ) by A4, XREAL_1:233 ; :: thesis: verum

consider m being marking of P such that

A2: for p being set st p in P holds

p multitude_of = H

take m ; :: thesis: for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of )

let p be set ; :: thesis: ( p in P implies p multitude_of = (p multitude_of ) - (p multitude_of ) )

assume A3: p in P ; :: thesis: p multitude_of = (p multitude_of ) - (p multitude_of )

then A4: p multitude_of >= p multitude_of by A1;

thus p multitude_of = (p multitude_of ) -' (p multitude_of ) by A2, A3

.= (p multitude_of ) - (p multitude_of ) by A4, XREAL_1:233 ; :: thesis: verum