let M be non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :], succ REAL ; :: thesis: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds Result [x,y],M = x + y )
assume A1: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [the InitS of M,[x,y]] = x + y ) ) ; :: thesis: for x, y being Element of REAL holds Result [x,y],M = x + y
let x, y be Real; :: thesis: Result [x,y],M = x + y
( x + y in succ REAL & [x,y] leads_to_final_state_of M & x + y is_result_of [x,y],M ) by A1, Def6, Th25, XBOOLE_0:def 3;
hence Result [x,y],M = x + y by Def9; :: thesis: verum