set M = I -TwoStatesMooreSM i,f,o;
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of (I -TwoStatesMooreSM i,f,o) = GEN w2,the InitS of (I -TwoStatesMooreSM i,f,o)

proof

let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN w1,the InitS of (I -TwoStatesMooreSM i,f,o) = GEN w2,the InitS of (I -TwoStatesMooreSM i,f,o) )
assume that
w1 . 1 = w2 . 1 and
A1: len w1 = len w2 ; :: thesis: GEN w1,the InitS of (I -TwoStatesMooreSM i,f,o) = GEN w2,the InitS of (I -TwoStatesMooreSM i,f,o)
reconsider p = GEN w1,the InitS of (I -TwoStatesMooreSM i,f,o), q = GEN w2,the InitS of (I -TwoStatesMooreSM i,f,o) as FinSequence ;
A2: p . 1 = the InitS of (I -TwoStatesMooreSM i,f,o) by FSM_1:def 2
.= q . 1 by FSM_1:def 2 ;
A3: len p = (len w1) + 1 by FSM_1:def 2;
A4: len q = (len w1) + 1 by A1, FSM_1:def 2;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len p implies p . j = q . j )
assume A5: 1 <= j ; :: thesis: ( j <= len p implies p . j = q . j )
A6: j in NAT by ORDINAL1:def 13;
( j = 1 or j > 1 ) by A5, XXREAL_0:1;
then not ( not p . j = q . j & j <= len p & not ( p . j = f & q . j = f ) ) by A1, A2, A3, A6, Th17;
hence ( j <= len p implies p . j = q . j ) ; :: thesis: verum

end;

hence GEN w1,the InitS of (I -TwoStatesMooreSM i,f,o) = GEN w2,the InitS of (I -TwoStatesMooreSM i,f,o) by A3, A4, FINSEQ_1:18; :: thesis: verum

end;

hence I -TwoStatesMooreSM i,f,o is calculating_type by Th7; :: thesis: verum