hereby :: thesis: ( ( for i being Element of I holds F . i is Group-like ) implies F is Group-like )

assume A2:
for i being Element of I holds F . i is Group-like
; :: thesis: F is Group-like assume A1:
F is Group-like
; :: thesis: for i being Element of I holds F . i is Group-like

let i be Element of I; :: thesis: F . i is Group-like

ex Fi being non empty Group-like multMagma st Fi = F . i by A1;

hence F . i is Group-like ; :: thesis: verum

end;let i be Element of I; :: thesis: F . i is Group-like

ex Fi being non empty Group-like multMagma st Fi = F . i by A1;

hence F . i is Group-like ; :: thesis: verum

let i be set ; :: according to GROUP_7:def 3 :: thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = F . i )

assume i in I ; :: thesis: ex Fi being non empty Group-like multMagma st Fi = F . i

then reconsider i1 = i as Element of I ;

reconsider F1 = F . i1 as non empty Group-like multMagma by A2;

take F1 ; :: thesis: F1 = F . i

thus F1 = F . i ; :: thesis: verum