thus
( m1 = m2 implies for p being object st p in P holds

p multitude_of = p multitude_of ) ; :: thesis: ( ( for p being object st p in P holds

p multitude_of = p multitude_of ) implies m1 = m2 )

A1: dom m1 = P by FUNCT_2:def 1;

dom m2 = P by FUNCT_2:def 1;

hence ( ( for p being object st p in P holds

p multitude_of = p multitude_of ) implies m1 = m2 ) by A1, FUNCT_1:2; :: thesis: verum

p multitude_of = p multitude_of ) ; :: thesis: ( ( for p being object st p in P holds

p multitude_of = p multitude_of ) implies m1 = m2 )

A1: dom m1 = P by FUNCT_2:def 1;

dom m2 = P by FUNCT_2:def 1;

hence ( ( for p being object st p in P holds

p multitude_of = p multitude_of ) implies m1 = m2 ) by A1, FUNCT_1:2; :: thesis: verum