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

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 .--> (succ (c . 0))) by A18
.= f2 . c by A23, A25 ; :: thesis: verum

end;

hence it1 = it2 by A15, A16, A19, A20, A21, A24, A17, A22, FUNCT_2:63; :: thesis: verum