let it1, it2 be strict AMI-Struct over N; :: thesis: ( 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 ; :: thesis: ( 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)))) ; :: thesis: ( 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 ; :: thesis: ( 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)))) ; :: thesis: it1 = it2
A23: the_Values_of it1 = the_Values_of it2 by A14, A15, A19, A20;

now :: thesis: for c being Element of product (the_Values_of it1) holds f1 . c = f2 . c

let c be Element of product (the_Values_of it1); :: thesis: f1 . c = f2 . c
thus f1 . c = c +* (0 .--> ((In ((c . 0),NAT)) + 1)) by A16
.= f2 . c by A21, A23 ; :: thesis: verum

end;

hence it1 = it2 by A13, A14, A17, A18, A19, A22, A15, A20, FUNCT_2:63; :: thesis: verum