let C1, C2 be Equivalence_Relation of M; :: thesis: ( ( for i being Element of I holds C1 . i = EqCl (R . i) ) & ( for i being Element of I holds C2 . i = EqCl (R . i) ) implies C1 = C2 )
assume that
A4: for i being Element of I holds C1 . i = EqCl (R . i) and
A5: for i being Element of I holds C2 . i = EqCl (R . i) ; :: thesis: C1 = C2

now :: thesis: for i being object st i in I holds
C1 . i = C2 . i

let i be object ; :: thesis: ( i in I implies C1 . i = C2 . i )
assume i in I ; :: thesis: C1 . i = C2 . i
then reconsider i1 = i as Element of I ;
thus C1 . i = EqCl (R . i1) by A4
.= C2 . i by A5 ; :: thesis: verum

end;

hence C1 = C2 by PBOOLE:3; :: thesis: verum