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

for S being non empty FSM over I

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

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

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

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

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

set w = <*s1,s2,s3*>;

reconsider w1 = <*s1,s2*>, w2 = <*s3*> as FinSequence of I ;

set Q = the Tran of S . [( the Tran of S . [q,s1]),s2];

A1: <*s1,s2,s3*> = w1 ^ w2 by FINSEQ_1:43;

A2: len w1 = 2 by FINSEQ_1:44;

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

then (GEN (w1,q)) . ((len w1) + 1) = the Tran of S . [( the Tran of S . [q,s1]),s2] by A2, FINSEQ_1:45;

then q,w1 -leads_to the Tran of S . [( the Tran of S . [q,s1]),s2] ;

then A3: GEN (<*s1,s2,s3*>,q) = (Del ((GEN (w1,q)),((len w1) + 1))) ^ (GEN (w2,( the Tran of S . [( the Tran of S . [q,s1]),s2]))) by A1, FSM_1:8;

Del ((GEN (w1,q)),((len w1) + 1)) = Del (<*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>,3) by A2, Th2

.= <*q,( the Tran of S . [q,s1])*> by WSIERP_1:19 ;

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

hence GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> by FINSEQ_4:74; :: thesis: verum

for S being non empty FSM over I

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

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

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

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

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

set w = <*s1,s2,s3*>;

reconsider w1 = <*s1,s2*>, w2 = <*s3*> as FinSequence of I ;

set Q = the Tran of S . [( the Tran of S . [q,s1]),s2];

A1: <*s1,s2,s3*> = w1 ^ w2 by FINSEQ_1:43;

A2: len w1 = 2 by FINSEQ_1:44;

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

then (GEN (w1,q)) . ((len w1) + 1) = the Tran of S . [( the Tran of S . [q,s1]),s2] by A2, FINSEQ_1:45;

then q,w1 -leads_to the Tran of S . [( the Tran of S . [q,s1]),s2] ;

then A3: GEN (<*s1,s2,s3*>,q) = (Del ((GEN (w1,q)),((len w1) + 1))) ^ (GEN (w2,( the Tran of S . [( the Tran of S . [q,s1]),s2]))) by A1, FSM_1:8;

Del ((GEN (w1,q)),((len w1) + 1)) = Del (<*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>,3) by A2, Th2

.= <*q,( the Tran of S . [q,s1])*> by WSIERP_1:19 ;

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

hence GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> by FINSEQ_4:74; :: thesis: verum