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 S1[ Nat] means ( \$1 <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . \$1 = f );
A4: S1[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 ; :: thesis: verum
end;
A5: for k being non trivial Nat st S1[k] holds
S1[k + 1]
proof
let k be non trivial Nat; :: thesis: ( S1[k] implies S1[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 ;
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 ;
hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f by ; :: thesis: verum
end;
A8: j is non trivial Nat by ;
for k being non trivial Nat holds S1[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