let n be Nat; for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n
let F be Subset of NAT; ( F = {n} implies LocSeq (F,S) = 0 .--> n )
assume A1:
F = {n}
; LocSeq (F,S) = 0 .--> n
then A2:
card F = {0}
by CARD_1:30, CARD_1:49;
{n} c= omega
by ORDINAL1:def 12;
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 Def1;
A5:
for a being object st a in dom (LocSeq (F,S)) holds
(LocSeq (F,S)) . a = (0 .--> n) . a
proof
let a be
object ;
( a in dom (LocSeq (F,S)) implies (LocSeq (F,S)) . a = (0 .--> n) . a )
assume A6:
a in dom (LocSeq (F,S))
;
(LocSeq (F,S)) . a = (0 .--> n) . a
then A7:
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, A6, Def1
.=
(0 .--> n) . a
by A1, A3, A7, FUNCOP_1:72
;
verum
end;
thus
LocSeq (F,S) = 0 .--> n
by A1, A4, A5, CARD_1:30, CARD_1:49; verum