let n be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated standard AMI-Struct of N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated standard AMI-Struct of N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let S be non empty IC-Ins-separated standard AMI-Struct of N; :: thesis: for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let F be Subset of NAT; :: thesis: ( F = {n} implies LocSeq (F,S) = 0 .--> n )
assume A1: F = {n} ; :: thesis: LocSeq (F,S) = 0 .--> n
then A2: card F = {0} by CARD_1:30, CARD_1:49;
{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 12; :: thesis: verum

end;

then A3: (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {n}))),(RelIncl {n}))) . 0 = (0 .--> n) . 0 by CARD_5:38
.= n by FUNCOP_1:72 ;
A4: dom (LocSeq (F,S)) = card F by Def3;
A5: F = {n} by A1;
A6: for a being set st a in dom (LocSeq (F,S)) holds
(LocSeq (F,S)) . a = (0 .--> n) . a

proof

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

end;

dom (0 .--> n) = {0} by FUNCOP_1:13;
hence LocSeq (F,S) = 0 .--> n by A1, A4, A6, CARD_1:30, CARD_1:49, FUNCT_1:2; :: thesis: verum