let it1, it2 be strict AMI-Struct over N; :: thesis: ( the carrier of it1 = & 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 ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) & the carrier of it2 = & 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 ()),(product ()) st
( ( for s being Element of product () holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of it2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ()))) ) implies it1 = it2 )

assume that
A13: ( the carrier of it1 = & 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 ()),(product ()) holds
( ex s being Element of product () 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 ()))) ) or not the carrier of it2 = 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 ()),(product ()) holds
( ex s being Element of product () 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 ()))) ) or it1 = it2 )

given f1 being Function of (product ()),(product ()) such that A16: for s being Element of product () 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 ()))) ; :: thesis: ( not the carrier of it2 = 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 ()),(product ()) holds
( ex s being Element of product () 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 ()))) ) or it1 = it2 )

assume that
A18: ( the carrier of it2 = & 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 ()),(product ()) holds
( ex s being Element of product () 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 ()))) ) or it1 = it2 )

given f2 being Function of (product ()),(product ()) such that A21: for s being Element of product () 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 ()))) ; :: 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 () holds f1 . c = f2 . c
let c be Element of product (); :: thesis: f1 . c = f2 . c
thus f1 . c = c +* (0 .--> ((In ((c . 0),NAT)) + 1)) by A16
.= f2 . c by ; :: thesis: verum
end;
hence it1 = it2 by ; :: thesis: verum