let n be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being Subset of NAT st F = {(il. S,n)} holds
LocSeq F,S = 0 .--> (il. S,n)
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being Subset of NAT st F = {(il. S,n)} holds
LocSeq F,S = 0 .--> (il. S,n)
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for F being Subset of NAT st F = {(il. S,n)} holds
LocSeq F,S = 0 .--> (il. S,n)
let F be Subset of NAT ; :: thesis: ( F = {(il. S,n)} implies LocSeq F,S = 0 .--> (il. S,n) )
assume A1: F = {(il. S,n)} ; :: thesis: LocSeq F,S = 0 .--> (il. S,n)
then A2: card F = {0 } by CARD_1:50, CARD_1:87;
{n} c= omega

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {n} or a in omega )
assume a in {n} ; :: thesis: a in omega
hence a in omega by ORDINAL1:def 13; :: thesis: verum

end;

then A3: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {n}))),(RelIncl {n})) . 0 = (0 .--> n) . 0 by Th15
.= n by FUNCOP_1:87 ;
A4: dom (LocSeq F,S) = card F by Def4;
A5: LocNums F,S = {n} by A1, Th26;
A6: for a being set st a in dom (LocSeq F,S) holds
(LocSeq F,S) . a = (0 .--> (il. S,n)) . a

proof

let a be set ; :: thesis: ( a in dom (LocSeq F,S) implies (LocSeq F,S) . a = (0 .--> (il. S,n)) . a )
assume A7: a in dom (LocSeq F,S) ; :: thesis: (LocSeq F,S) . a = (0 .--> (il. S,n)) . a
then A8: a = 0 by A4, A2, TARSKI:def 1;
thus (LocSeq F,S) . a = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums F,S)))),(RelIncl (LocNums F,S))) . a) by A4, A7, Def4
.= (0 .--> (il. S,n)) . a by A5, A3, A8, FUNCOP_1:87 ; :: thesis: verum

end;

dom (0 .--> (il. S,n)) = {0 } by FUNCOP_1:19;
hence LocSeq F,S = 0 .--> (il. S,n) by A1, A4, A6, CARD_1:50, CARD_1:87, FUNCT_1:9; :: thesis: verum