let I, O be non empty set ; :: thesis: for w being FinSequence of I
for i, f being set
for o being Function of {i,f},O
for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let w be FinSequence of I; :: thesis: for i, f being set
for o being Function of {i,f},O
for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let i, f be set ; :: thesis: for o being Function of {i,f},O
for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let o be Function of {i,f},O; :: thesis: for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f
let j be non zero Element of NAT ; :: thesis: ( 1 < j & j <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f )
assume A1: 1 < j ; :: thesis: ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f )
set M = I -TwoStatesMooreSM (i,f,o);
A2: the carrier of (I -TwoStatesMooreSM (i,f,o)) = {i,f} by Def7;
A3: the Tran of (I -TwoStatesMooreSM (i,f,o)) = [:{i,f},I:] --> f by Def7;
defpred S₁[ Nat] means ( $1 <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . $1 = f );
A4: S₁[2]

proof

assume 2 <= (len w) + 1 ; :: thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f
then 1 + 1 <= (len w) + 1 ;
then 1 < (len w) + 1 by NAT_1:13;
then 1 <= len w by NAT_1:13;
then ex WI being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st
( WI = w . 1 & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 1 & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def 2;
hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f by A2, A3, FUNCOP_1:7; :: thesis: verum

end;

A5: for k being non trivial Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non trivial Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
( k <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k = f ) and
A6: k + 1 <= (len w) + 1 ; :: thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f
A7: 1 <= k by NAT_2:19;
k <= len w by A6, XREAL_1:6;
then ex WI being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st
( WI = w . k & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) & WI -succ_of QI = QI1 ) by A7, FSM_1:def 2;
hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f by A2, A3, FUNCOP_1:7; :: thesis: verum

end;

A8: j is non trivial Nat by A1, NAT_2:def 1;
for k being non trivial Nat holds S₁[k] from NAT_2:sch 2(A4, A5);
hence ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) by A8; :: thesis: verum