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)))

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

hence
I -TwoStatesMooreSM (i,f,o) is calculating_type
by Th7; :: thesis: verum
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;

end;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 :: thesis: for j being Nat st 1 <= j & j <= len p holds

p . j = q . j

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:14; :: thesis: verump . j = q . j

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 12;

( 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;assume A5: 1 <= j ; :: thesis: ( j <= len p implies p . j = q . j )

A6: j in NAT by ORDINAL1:def 12;

( 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