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

assume A6:
for i being Element of I holds F . i is commutative
; :: thesis: F is commutative assume A5:
F is commutative
; :: thesis: for i being Element of I holds F . i is commutative

let i be Element of I; :: thesis: F . i is commutative

ex Fi being non empty commutative multMagma st Fi = F . i by A5;

hence F . i is commutative ; :: thesis: verum

end;let i be Element of I; :: thesis: F . i is commutative

ex Fi being non empty commutative multMagma st Fi = F . i by A5;

hence F . i is commutative ; :: thesis: verum

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

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

then reconsider i1 = i as Element of I ;

reconsider Fi = F . i1 as non empty commutative multMagma by A6;

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

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