thus for A, B being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds A . i = (Omega). (F . i) ) & ( for i being Element of I holds B . i = (Omega). (F . i) ) holds
A = B :: thesis: verum

proof

let A, B be componentwise_strict Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds A . i = (Omega). (F . i) ) & ( for i being Element of I holds B . i = (Omega). (F . i) ) implies A = B )
assume A1: for i being Element of I holds A . i = (Omega). (F . i) ; :: thesis: ( ex i being Element of I st not B . i = (Omega). (F . i) or A = B )
assume A2: for i being Element of I holds B . i = (Omega). (F . i) ; :: thesis: A = B
for i being Element of I holds A . i = B . i

proof

let i be Element of I; :: thesis: A . i = B . i
thus A . i = (Omega). (F . i) by A1
.= B . i by A2 ; :: thesis: verum

end;

hence A = B by ThStrSubEq; :: thesis: verum

end;