set O = {0};
set V = N --> NAT;
reconsider IC1 = 0 as Element of {0} by TARSKI:def 1;
reconsider i = [0,0,0] as Element of {[1,{},{}],[0,{},{}]} by TARSKI:def 2;
A1: 0 in N by MEASURE6:def 2;
then A2: (N --> NAT) * (0 .--> 0) = 0 .--> NAT by FUNCOP_1:89;
then A3: dom ((N --> NAT) * (0 .--> 0)) = {0} ;
A4: dom (0 .--> 0) = {0} ;
rng (0 .--> 0) = {0} by FUNCOP_1:88;
then rng (0 .--> 0) c= N by A1, ZFMISC_1:31;
then reconsider Ok = 0 .--> 0 as Function of {0},N by A4, RELSET_1:4;
deffunc H₁( Element of product ((N --> NAT) * Ok)) -> set = $1 +* (0 .--> ((In (($1 . 0),NAT)) + 1));

A5: now :: thesis: for s being Element of product ((N --> NAT) * Ok) holds H₁(s) in product ((N --> NAT) * Ok)

let s be Element of product ((N --> NAT) * Ok); :: thesis: H₁(s) in product ((N --> NAT) * Ok)

now :: thesis: ( dom (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) = dom ((N --> NAT) * Ok) & ( for o being object st o in dom ((N --> NAT) * Ok) holds
(s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o in ((N --> NAT) * Ok) . o ) )

thus dom (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) = (dom s) \/ (dom (0 .--> ((In ((s . 0),NAT)) + 1))) by FUNCT_4:def 1
.= (dom s) \/ {0}
.= {0} \/ {0} by PARTFUN1:def 2
.= dom ((N --> NAT) * Ok) by A3 ; :: thesis: for o being object st o in dom ((N --> NAT) * Ok) holds
(s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o in ((N --> NAT) * Ok) . o
let o be object ; :: thesis: ( o in dom ((N --> NAT) * Ok) implies (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o in ((N --> NAT) * Ok) . o )
A6: dom (0 .--> ((In ((s . 0),NAT)) + 1)) = {0} ;
assume A7: o in dom ((N --> NAT) * Ok) ; :: thesis: (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o in ((N --> NAT) * Ok) . o
A8: ((N --> NAT) * Ok) . o = NAT by A7, A2, FUNCOP_1:7;
(s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o = (0 .--> ((In ((s . 0),NAT)) + 1)) . o by A6, A7, FUNCT_4:13
.= (In ((s . 0),NAT)) + 1 by A7, FUNCOP_1:7 ;
hence (s +* (0 .--> ((In ((s . 0),NAT)) + 1))) . o in ((N --> NAT) * Ok) . o by A8; :: thesis: verum

end;

hence H₁(s) in product ((N --> NAT) * Ok) by CARD_3:9; :: thesis: verum

end;

consider f being Function of (product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)) such that
A9: for s being Element of product ((N --> NAT) * Ok) holds f . s = H₁(s) from FUNCT_2:sch 8(A5);
set E = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))));
A10: dom (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) = (dom ([1,0,0] .--> f)) \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) by FUNCT_4:def 1
.= {[1,0,0]} \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))))
.= {[1,0,0]} \/ {[0,0,0]}
.= {[1,{},{}],[0,{},{}]} by ENUMSET1:1 ;
A11: ( rng ([1,0,0] .--> f) c= {f} & rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) c= {(id (product ((N --> NAT) * Ok)))} ) by FUNCOP_1:13;
A12: rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) c= (rng ([1,0,0] .--> f)) \/ (rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) by FUNCT_4:17;
rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) c= Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) or e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) )
assume e in rng (([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok))))) ; :: thesis: e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)))
then ( e in rng ([1,0,0] .--> f) or e in rng ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) ) by A12, XBOOLE_0:def 3;
then ( e = f or e = id (product ((N --> NAT) * Ok)) ) by A11, TARSKI:def 1;
hence e in Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok))) by FUNCT_2:9; :: thesis: verum

end;

then reconsider E = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product ((N --> NAT) * Ok)))) as Function of {[1,{},{}],[0,{},{}]},(Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)))) by A10, FUNCT_2:def 1, RELSET_1:4;
set V = N --> NAT;
set M = AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #);
take AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) ; :: thesis: ( the carrier of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {0} & IC = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ) )
thus the carrier of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {0} ; :: thesis: ( IC = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ) )
thus IC = 0 ; :: thesis: ( the InstructionsF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ) )
thus the InstructionsF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} ; :: thesis: ( the Object-Kind of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ) )
thus the Object-Kind of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = 0 .--> 0 ; :: thesis: ( the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ) )
thus the ValuesF of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = N --> NAT ; :: thesis: ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) )
reconsider f = f as Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))) ;
take f ; :: thesis: ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) )
thus for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) by A9; :: thesis: the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #)))))
thus the Execution of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,{},{}],[0,{},{}]},Ok,(N --> NAT),E #))))) ; :: thesis: verum