let I be non empty set ; :: thesis: for S being non empty FSM over 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 over 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:4; :: thesis: verum