let n be Nat; :: thesis: 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 ; :: thesis: 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; :: 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 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

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 ; :: thesis: 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; :: 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 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

thus
LocSeq (F,S) = 0 .--> n
by A1, A4, A5, CARD_1:30, CARD_1:49; :: thesis: verum
let a be object ; :: thesis: ( a in dom (LocSeq (F,S)) implies (LocSeq (F,S)) . a = (0 .--> n) . a )

assume A6: a in dom (LocSeq (F,S)) ; :: thesis: (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 ; :: thesis: verum

end;assume A6: a in dom (LocSeq (F,S)) ; :: thesis: (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 ; :: thesis: verum