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

assume A3: F is associative ; :: thesis: for i being Element of I holds F . i is associative
let i be Element of I; :: thesis: F . i is associative
ex Fi being non empty associative multMagma st Fi = F . i by A3;
hence F . i is associative ; :: thesis: verum

end;

assume A4: for i being Element of I holds F . i is associative ; :: thesis: F is associative
let i be set ; :: according to GROUP_7:def 4 :: thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = F . i )
assume i in I ; :: thesis: ex Fi being non empty associative multMagma st Fi = F . i
then reconsider i1 = i as Element of I ;
reconsider Fi = F . i1 as non empty associative multMagma by A4;
take Fi ; :: thesis: Fi = F . i
thus Fi = F . i ; :: thesis: verum