let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM over 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 over I
for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>
let S be non empty FSM over 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:39;
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:39;
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:40;
hence GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> by A2, A3, A5, A6, A7, FINSEQ_1:44; :: thesis: verum