:: deftheorem Def3 defines Product GROUP_9:def 3 :
for O, E being set
for A being Action of O,E
for F being FinSequence of O
for b₅ being Function of E,E holds
( ( len F = 0 implies ( b₅ = Product (F,A) iff b₅ = id E ) ) & ( not len F = 0 implies ( b₅ = Product (F,A) iff ex PF being FinSequence of Funcs (E,E) st
( b₅ = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) );