let m be marking of P; :: thesis: ( m = m1 + m2 iff for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) )

thus ( m = m1 + m2 implies for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ) by VALUED_1:1; :: thesis: ( ( for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ) implies m = m1 + m2 )

assume A1: for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ; :: thesis: m = m1 + m2

A2: dom m = P by FUNCT_2:def 1;

A3: dom (m1 + m2) = (dom m1) /\ (dom m2) by VALUED_1:def 1

.= P /\ (dom m2) by FUNCT_2:def 1

.= P /\ P by FUNCT_2:def 1 ;

p multitude_of = (p multitude_of ) + (p multitude_of ) )

thus ( m = m1 + m2 implies for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ) by VALUED_1:1; :: thesis: ( ( for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ) implies m = m1 + m2 )

assume A1: for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) ; :: thesis: m = m1 + m2

A2: dom m = P by FUNCT_2:def 1;

A3: dom (m1 + m2) = (dom m1) /\ (dom m2) by VALUED_1:def 1

.= P /\ (dom m2) by FUNCT_2:def 1

.= P /\ P by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom m holds

m . x = (m1 + m2) . x

hence
m = m1 + m2
by A2, A3, FUNCT_1:2; :: thesis: verumm . x = (m1 + m2) . x

let x be object ; :: thesis: ( x in dom m implies m . x = (m1 + m2) . x )

assume A4: x in dom m ; :: thesis: m . x = (m1 + m2) . x

hence m . x = (m1 . x) + (m2 . x) by A1, A2

.= (m1 + m2) . x by A2, A3, A4, VALUED_1:def 1 ;

:: thesis: verum

end;assume A4: x in dom m ; :: thesis: m . x = (m1 + m2) . x

hence m . x = (m1 . x) + (m2 . x) by A1, A2

.= (m1 + m2) . x by A2, A3, A4, VALUED_1:def 1 ;

:: thesis: verum