let I be non empty set ; :: thesis: for s1, s2 being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let s1, s2 be Element of I; :: thesis: for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let S be non empty FSM over I; :: thesis: for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let q be State of S; :: thesis: GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

set w = <*s1,s2*>;

A1: (GEN (<*s1,s2*>,q)) . 1 = q by FSM_1:def 2;

A2: <*s1,s2*> = <*s1*> ^ <*s2*> by FINSEQ_1:def 9;

A3: len <*s1*> = 1 by FINSEQ_1:39;

GEN (<*s1*>,q) = <*q,( the Tran of S . [q,s1])*> by Th1;

then (GEN (<*s1*>,q)) . (1 + 1) = the Tran of S . [q,s1] by FINSEQ_1:44;

then q,<*s1*> -leads_to the Tran of S . [q,s1] by A3;

then A4: (GEN (<*s1,s2*>,q)) . (1 + 1) = the Tran of S . [q,s1] by A2, A3, FSM_1:6;

A5: len <*s1,s2*> = 2 by FINSEQ_1:44;

2 <= len <*s1,s2*> by FINSEQ_1:44;

then consider WI being Element of I, QI, QI1 being State of S such that

A6: WI = <*s1,s2*> . 2 and

A7: QI = (GEN (<*s1,s2*>,q)) . 2 and

A8: QI1 = (GEN (<*s1,s2*>,q)) . (2 + 1) and

A9: WI -succ_of QI = QI1 by FSM_1:def 2;

A10: WI = s2 by A6, FINSEQ_1:44;

len (GEN (<*s1,s2*>,q)) = (len <*s1,s2*>) + 1 by FSM_1:def 2

.= 3 by A5 ;

hence GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by A1, A4, A7, A8, A9, A10, FINSEQ_1:45; :: thesis: verum

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let s1, s2 be Element of I; :: thesis: for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let S be non empty FSM over I; :: thesis: for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

let q be State of S; :: thesis: GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

set w = <*s1,s2*>;

A1: (GEN (<*s1,s2*>,q)) . 1 = q by FSM_1:def 2;

A2: <*s1,s2*> = <*s1*> ^ <*s2*> by FINSEQ_1:def 9;

A3: len <*s1*> = 1 by FINSEQ_1:39;

GEN (<*s1*>,q) = <*q,( the Tran of S . [q,s1])*> by Th1;

then (GEN (<*s1*>,q)) . (1 + 1) = the Tran of S . [q,s1] by FINSEQ_1:44;

then q,<*s1*> -leads_to the Tran of S . [q,s1] by A3;

then A4: (GEN (<*s1,s2*>,q)) . (1 + 1) = the Tran of S . [q,s1] by A2, A3, FSM_1:6;

A5: len <*s1,s2*> = 2 by FINSEQ_1:44;

2 <= len <*s1,s2*> by FINSEQ_1:44;

then consider WI being Element of I, QI, QI1 being State of S such that

A6: WI = <*s1,s2*> . 2 and

A7: QI = (GEN (<*s1,s2*>,q)) . 2 and

A8: QI1 = (GEN (<*s1,s2*>,q)) . (2 + 1) and

A9: WI -succ_of QI = QI1 by FSM_1:def 2;

A10: WI = s2 by A6, FINSEQ_1:44;

len (GEN (<*s1,s2*>,q)) = (len <*s1,s2*>) + 1 by FSM_1:def 2

.= 3 by A5 ;

hence GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by A1, A4, A7, A8, A9, A10, FINSEQ_1:45; :: thesis: verum