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 ;

now :: thesis: for x being object st x in dom m holds
m . 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;

hence m = m1 + m2 by A2, A3, FUNCT_1:2; :: thesis: verum