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