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 ],[1,0 ]} & the Object-Kind of it1 = (NAT --> {[1,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 ] .--> f) +* ([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 ],[1,0 ]} & the Object-Kind of it2 = (NAT --> {[1,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 ] .--> f) +* ([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 ],[1,0 ]} ) and
A17: the Object-Kind of it1 = (NAT --> {[1,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 ] .--> f) +* ([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 ],[1,0 ]} or not the Object-Kind of it2 = (NAT --> {[1,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 ] .--> f) +* ([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 ] .--> f1) +* ([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 ],[1,0 ]} or not the Object-Kind of it2 = (NAT --> {[1,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 ] .--> f) +* ([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 ],[1,0 ]} ) and
A21: the Object-Kind of it2 = (NAT --> {[1,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 ] .--> f) +* ([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 ] .--> f2) +* ([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