let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM of I
for q being State of S holds GEN <*s*>,q = <*q,(the Tran of S . [q,s])*>
let s be Element of I; :: thesis: for S being non empty FSM of I
for q being State of S holds GEN <*s*>,q = <*q,(the Tran of S . [q,s])*>
let S be non empty FSM of I; :: thesis: for q being State of S holds GEN <*s*>,q = <*q,(the Tran of S . [q,s])*>
let q be State of S; :: thesis: GEN <*s*>,q = <*q,(the Tran of S . [q,s])*>
A1: len <*s*> = 1 by FINSEQ_1:56;
A2: len (GEN <*s*>,q) = (len <*s*>) + 1 by FSM_1:def 2
.= 2 by A1 ;
A3: (GEN <*s*>,q) . 1 = q by FSM_1:def 2;
1 <= len <*s*> by FINSEQ_1:56;
then consider WI being Element of I, QI, QI1 being State of S such that
A4: WI = <*s*> . 1 and
A5: QI = (GEN <*s*>,q) . 1 and
A6: QI1 = (GEN <*s*>,q) . (1 + 1) and
A7: WI -succ_of QI = QI1 by FSM_1:def 2;
WI = s by A4, FINSEQ_1:57;
hence GEN <*s*>,q = <*q,(the Tran of S . [q,s])*> by A2, A3, A5, A6, A7, FINSEQ_1:61; :: thesis: verum