let I be non empty set ; :: thesis: for s1, s2, s3 being Element of I
for S being non empty FSM of 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 of 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 of 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:60;
A2: len w1 = 2 by FINSEQ_1:61;
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:62;
then q,w1 -leads_to the Tran of S . [(the Tran of S . [q,s1]),s2] by FSM_1:def 3;
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:23;
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:26 ;
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:89; :: thesis: verum