let it1, it2 be strict AMI-Struct of N; :: thesis: ( the carrier of it1 = {0} & the ZeroF of it1 = 0 & the Instructions of it1 = {[0,0,0],[1,0,0]} & the haltF of it1 = [0,0,0] & the Object-Kind of it1 = 0 .--> NAT & ex f being Function of (product the Object-Kind of it1),(product the Object-Kind of it1) st
( ( for s being Element of product the Object-Kind of it1 holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it1))) ) & the carrier of it2 = {0} & the ZeroF of it2 = 0 & the Instructions of it2 = {[0,0,0],[1,0,0]} & the haltF of it2 = [0,0,0] & the Object-Kind of it2 = 0 .--> NAT & ex f being Function of (product the Object-Kind of it2),(product the Object-Kind of it2) st
( ( for s being Element of product the Object-Kind of it2 holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ) implies it1 = it2 )
assume that
A17: ( the carrier of it1 = {0} & the ZeroF of it1 = 0 & the Instructions of it1 = {[0,0,0],[1,0,0]} & the haltF of it1 = [0,0,0] ) and
A18: the Object-Kind of it1 = 0 .--> NAT ; :: thesis: ( for f being Function of (product the Object-Kind of it1),(product the Object-Kind of it1) holds
( ex s being Element of product the Object-Kind of it1 st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it1))) ) or not the carrier of it2 = {0} or not the ZeroF of it2 = 0 or not the Instructions of it2 = {[0,0,0],[1,0,0]} or not the haltF of it2 = [0,0,0] or not the Object-Kind of it2 = 0 .--> NAT or for f being Function of (product the Object-Kind of it2),(product the Object-Kind of it2) holds
( ex s being Element of product the Object-Kind of it2 st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ) or it1 = it2 )
given f1 being Function of (product the Object-Kind of it1),(product the Object-Kind of it1) such that A19: for s being Element of product the Object-Kind of it1 holds f1 . s = s +* (0 .--> (succ (s . 0))) and
A20: the Execution of it1 = ([1,0,0] .--> f1) +* ([0,0,0] .--> (id (product the Object-Kind of it1))) ; :: thesis: ( not the carrier of it2 = {0} or not the ZeroF of it2 = 0 or not the Instructions of it2 = {[0,0,0],[1,0,0]} or not the haltF of it2 = [0,0,0] or not the Object-Kind of it2 = 0 .--> NAT or for f being Function of (product the Object-Kind of it2),(product the Object-Kind of it2) holds
( ex s being Element of product the Object-Kind of it2 st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ) or it1 = it2 )
assume that
A21: ( the carrier of it2 = {0} & the ZeroF of it2 = 0 & the Instructions of it2 = {[0,0,0],[1,0,0]} & the haltF of it2 = [0,0,0] ) and
A22: the Object-Kind of it2 = 0 .--> NAT ; :: thesis: ( for f being Function of (product the Object-Kind of it2),(product the Object-Kind of it2) holds
( ex s being Element of product the Object-Kind of it2 st not f . s = s +* (0 .--> (succ (s . 0))) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ) or it1 = it2 )
given f2 being Function of (product the Object-Kind of it2),(product the Object-Kind of it2) such that A23: for s being Element of product the Object-Kind of it2 holds f2 . s = s +* (0 .--> (succ (s . 0))) and
A24: the Execution of it2 = ([1,0,0] .--> f2) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ; :: thesis: it1 = it2

now

let c be Element of product the Object-Kind of it1; :: thesis: f1 . c = f2 . c
thus f1 . c = c +* (0 .--> (succ (c . 0))) by A19
.= f2 . c by A18, A22, A23 ; :: thesis: verum

end;

hence it1 = it2 by A17, A18, A20, A21, A22, A24, FUNCT_2:63; :: thesis: verum