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

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

hence
C1 = C2
by PBOOLE:3; :: thesis: verumC1 . 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;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