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

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