let it1, it2 be strict AMI-Struct of N; :: thesis: ( the carrier of it1 = NAT \/ {NAT} & the Instruction-Counter of it1 = NAT & the Instructions of it1 = {[0,0,0],[1,0,0]} & the haltF of it1 = [0,0,0] & the Object-Kind of it1 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) ) & the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it1))) ) & the carrier of it2 = NAT \/ {NAT} & the Instruction-Counter of it2 = NAT & the Instructions of it2 = {[0,0,0],[1,0,0]} & the haltF of it2 = [0,0,0] & the Object-Kind of it2 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) ) & the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of it2))) ) implies it1 = it2 )
assume that
A16: ( the carrier of it1 = NAT \/ {NAT} & the Instruction-Counter of it1 = NAT & the Instructions of it1 = {[0,0,0],[1,0,0]} & the haltF of it1 = [0,0,0] ) and
A17: the Object-Kind of it1 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) 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 = NAT \/ {NAT} or not the Instruction-Counter of it2 = NAT 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 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) 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 A18: for s being Element of product the Object-Kind of it1 holds f1 . s = s +* (NAT .--> (succ (s . NAT))) and
A19: the Execution of it1 = ([1,0,0] .--> f1) +* ([0,0,0] .--> (id (product the Object-Kind of it1))) ; :: thesis: ( not the carrier of it2 = NAT \/ {NAT} or not the Instruction-Counter of it2 = NAT 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 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) 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
A20: ( the carrier of it2 = NAT \/ {NAT} & the Instruction-Counter of it2 = NAT & the Instructions of it2 = {[0,0,0],[1,0,0]} & the haltF of it2 = [0,0,0] ) and
A21: the Object-Kind of it2 = (NAT --> {[1,0,0],[0,0,0]}) +* (NAT .--> 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 +* (NAT .--> (succ (s . NAT))) 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 A22: for s being Element of product the Object-Kind of it2 holds f2 . s = s +* (NAT .--> (succ (s . NAT))) and
A23: 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 +* (NAT .--> (succ (c . NAT))) by A18
.= f2 . c by A17, A21, A22 ; :: thesis: verum

end;

hence it1 = it2 by A16, A17, A19, A20, A21, A23, FUNCT_2:113; :: thesis: verum