let O be non empty set ; :: thesis: for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o
let E be set ; :: thesis: for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o
let o be Element of O; :: thesis: for A being Action of O,E holds Product (<*o*>,A) = A . o
let A be Action of O,E; :: thesis: Product (<*o*>,A) = A . o
( len <*o*> = 1 & ex PF being FinSequence of Funcs (E,E) st
( Product (<*o*>,A) = PF . (len <*o*>) & len PF = len <*o*> & PF . 1 = A . (<*o*> . 1) & ( for k being Nat st k <> 0 & k < len <*o*> holds
ex f, g being Function of E,E st
( f = PF . k & g = A . (<*o*> . (k + 1)) & PF . (k + 1) = f * g ) ) ) ) by Def3, FINSEQ_1:39;
hence Product (<*o*>,A) = A . o by FINSEQ_1:40; :: thesis: verum