thus for A, B being Group-Family of I st ( for i being Element of I holds A . i = (F . i) ./. (N . i) ) & ( for i being Element of I holds B . i = (F . i) ./. (N . i) ) holds
A = B :: thesis: verum

proof

let A, B be Group-Family of I; :: thesis: ( ( for i being Element of I holds A . i = (F . i) ./. (N . i) ) & ( for i being Element of I holds B . i = (F . i) ./. (N . i) ) implies A = B )
assume A1: for i being Element of I holds A . i = (F . i) ./. (N . i) ; :: thesis: ( ex i being Element of I st not B . i = (F . i) ./. (N . i) or A = B )
assume A2: for i being Element of I holds B . i = (F . i) ./. (N . i) ; :: thesis: A = B
for i being object st i in I holds
A . i = B . i

proof

let i be object ; :: thesis: ( i in I implies A . i = B . i )
assume i in I ; :: thesis: A . i = B . i
then reconsider j = i as Element of I ;
A . j = (F . j) ./. (N . j) by A1
.= B . j by A2 ;
hence A . i = B . i ; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum

end;