let it1, it2 be strict AMI-Struct over N; ( the carrier of it1 = {0} & IC = 0 & the InstructionsF of it1 = {[0,0,0],[1,0,0]} & the Object-Kind of it1 = 0 .--> 0 & the ValuesF of it1 = N --> NAT & ex f being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) st
( ( for s being Element of product (the_Values_of it1) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it1)))) ) & the carrier of it2 = {0} & IC = 0 & the InstructionsF of it2 = {[0,0,0],[1,0,0]} & the Object-Kind of it2 = 0 .--> 0 & the ValuesF of it2 = N --> NAT & ex f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) st
( ( for s being Element of product (the_Values_of it2) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) implies it1 = it2 )
assume that
A13:
( the carrier of it1 = {0} & IC = 0 & the InstructionsF of it1 = {[0,0,0],[1,0,0]} )
and
A14:
the Object-Kind of it1 = 0 .--> 0
and
A15:
the ValuesF of it1 = N --> NAT
; ( for f being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) holds
( ex s being Element of product (the_Values_of it1) st not f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) or not the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it1)))) ) or not the carrier of it2 = {0} or not IC = 0 or not the InstructionsF of it2 = {[0,0,0],[1,0,0]} or not the Object-Kind of it2 = 0 .--> 0 or not the ValuesF of it2 = N --> NAT or for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds
( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 )
given f1 being Function of (product (the_Values_of it1)),(product (the_Values_of it1)) such that A16:
for s being Element of product (the_Values_of it1) holds f1 . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1))
and
A17:
the Execution of it1 = ([1,0,0] .--> f1) +* ([0,0,0] .--> (id (product (the_Values_of it1))))
; ( not the carrier of it2 = {0} or not IC = 0 or not the InstructionsF of it2 = {[0,0,0],[1,0,0]} or not the Object-Kind of it2 = 0 .--> 0 or not the ValuesF of it2 = N --> NAT or for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds
( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 )
assume that
A18:
( the carrier of it2 = {0} & IC = 0 & the InstructionsF of it2 = {[0,0,0],[1,0,0]} )
and
A19:
the Object-Kind of it2 = 0 .--> 0
and
A20:
the ValuesF of it2 = N --> NAT
; ( for f being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) holds
( ex s being Element of product (the_Values_of it2) st not f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) or not the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it2)))) ) or it1 = it2 )
given f2 being Function of (product (the_Values_of it2)),(product (the_Values_of it2)) such that A21:
for s being Element of product (the_Values_of it2) holds f2 . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1))
and
A22:
the Execution of it2 = ([1,0,0] .--> f2) +* ([0,0,0] .--> (id (product (the_Values_of it2))))
; it1 = it2
A23:
the_Values_of it1 = the_Values_of it2
by A14, A15, A19, A20;
hence
it1 = it2
by A13, A14, A17, A18, A19, A22, A15, A20, FUNCT_2:63; verum