thus ( A = B implies for i being Element of I holds A . i = B . i ) ; :: thesis: ( ( for i being Element of I holds A . i = B . i ) implies A = B )
assume for i being Element of I holds A . i = B . i ; :: thesis: A = B
then for i being set st i in I holds
A . i = B . i ;
hence A = B by Th3; :: thesis: verum