let M be non empty calculating_type halting Moore-SM_Final over [: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 that

A1: the carrier of M = succ REAL and

A2: the FinalS of M = REAL and

A3: the InitS of M = REAL and

A4: the OFun of M = id the carrier of M and

A5: 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 Element of REAL ; :: thesis: Result ([x,y],M) = x + y

A6: x + y in succ REAL by XBOOLE_0:def 3;

x + y is_result_of [x,y],M by A1, A2, A3, A4, A5, Th25;

hence Result ([x,y],M) = x + y by A6, Def9; :: thesis: verum

assume that

A1: the carrier of M = succ REAL and

A2: the FinalS of M = REAL and

A3: the InitS of M = REAL and

A4: the OFun of M = id the carrier of M and

A5: 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 Element of REAL ; :: thesis: Result ([x,y],M) = x + y

A6: x + y in succ REAL by XBOOLE_0:def 3;

x + y is_result_of [x,y],M by A1, A2, A3, A4, A5, Th25;

hence Result ([x,y],M) = x + y by A6, Def9; :: thesis: verum