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,0],[0,0,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} by FUNCOP_1:13;
A4: dom (0 .--> 0) = {0} by FUNCOP_1:13;
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 .--> (succ ($1 . 0)));

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 .--> (succ (s . 0)))) = dom ((N --> NAT) * Ok) & ( for o being set st o in dom ((N --> NAT) * Ok) holds
(s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o ) )

thus dom (s +* (0 .--> (succ (s . 0)))) = (dom s) \/ (dom (0 .--> (succ (s . 0)))) by FUNCT_4:def 1
.= (dom s) \/ {0} by FUNCOP_1:13
.= {0} \/ {0} by PARTFUN1:def 2
.= dom ((N --> NAT) * Ok) by A3 ; :: thesis: for o being set st o in dom ((N --> NAT) * Ok) holds
(s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o
let o be set ; :: thesis: ( o in dom ((N --> NAT) * Ok) implies (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o )
A6: dom (0 .--> (succ (s . 0))) = {0} by FUNCOP_1:13;
assume A7: o in dom ((N --> NAT) * Ok) ; :: thesis: (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o
A8: o = 0 by A7, TARSKI:def 1;
A9: ((N --> NAT) * Ok) . o = NAT by A7, A2, FUNCOP_1:7;
A10: (s +* (0 .--> (succ (s . 0)))) . o = (0 .--> (succ (s . 0))) . o by A6, A7, FUNCT_4:13
.= succ (s . 0) by A7, FUNCOP_1:7 ;
0 in dom ((N --> NAT) * Ok) by A3, TARSKI:def 1;
then reconsider k = s . 0 as Element of NAT by A8, A9, CARD_3:9;
succ k in NAT ;
hence (s +* (0 .--> (succ (s . 0)))) . o in ((N --> NAT) * Ok) . o by A9, A10; :: 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
A11: 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))));
A12: 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))))) by FUNCOP_1:13
.= {[1,0,0]} \/ {[0,0,0]} by FUNCOP_1:13
.= {[1,0,0],[0,0,0]} by ENUMSET1:1 ;
A13: ( 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;
A14: 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 set ; :: 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 A14, XBOOLE_0:def 3;
then ( e = f or e = id (product ((N --> NAT) * Ok)) ) by A13, 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,0],[0,0,0]},(Funcs ((product ((N --> NAT) * Ok)),(product ((N --> NAT) * Ok)))) by A12, FUNCT_2:def 1, RELSET_1:4;
set V = N --> NAT;
set M = AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #);
take AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) ; :: thesis: ( the carrier of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {0} & the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) )
thus the carrier of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {0} ; :: thesis: ( the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 & the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) )
thus the ZeroF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 ; :: thesis: ( the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} & the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) )
thus the InstructionsF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = {[0,0,0],[1,0,0]} ; :: thesis: ( the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 & the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) )
thus the Object-Kind of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = 0 .--> 0 ; :: thesis: ( the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT & ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ) )
thus the ValuesF of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = N --> NAT ; :: thesis: ex f being Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) st
( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) )
reconsider f = f as Function of (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))),(product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))) ;
take f ; :: thesis: ( ( for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) )
thus for s being Element of product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)) holds f . s = s +* (0 .--> (succ (s . 0))) by A11; :: thesis: the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #)))))
thus the Execution of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},IC1,{[1,0,0],[0,0,0]},Ok,(N --> NAT),E #))))) ; :: thesis: verum