let I be non empty set ; :: thesis: for S being non empty FSM of I st S is calculating_type holds
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S
let S be non empty FSM of I; :: thesis: ( S is calculating_type implies for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S )
assume A1: S is calculating_type ; :: thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN w1,the InitS of S = GEN w2,the InitS of S )
assume that
A2: w1 . 1 = w2 . 1 and
A3: len w1 = len w2 ; :: thesis: GEN w1,the InitS of S = GEN w2,the InitS of S
A4: len (GEN w1,the InitS of S) = 1 + (len w1) by FSM_1:def 2;
len (GEN w2,the InitS of S) = 1 + (len w2) by FSM_1:def 2;
hence GEN w1,the InitS of S = GEN w2,the InitS of S by A1, A2, A3, A4, Th4, TREES_1:19; :: thesis: verum