let V, A be set ; :: thesis:
let i, j, b, n, s be Element of V; :: thesis:
let i1, j1, b1, n1, s1 be object ; :: thesis:
let d1, Li, Lj, Lb, Ln, Ls be NonatomicND of V,A; :: thesis:
let Di, Dj, Db, Dn, Ds be SCBinominativeFunction of V,A; :: thesis:
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: ( Di = denaming (V,A,i1) & Dj = denaming (V,A,j1) & Db = denaming (V,A,b1) & Dn = denaming (V,A,n1) & Ds = denaming (V,A,s1) & Li = local_overlapping (V,A,d1,(Di . d1),i) & Lj = local_overlapping (V,A,Li,(Dj . Li),j) & Lb = local_overlapping (V,A,Lj,(Db . Lj),b) & Ln = local_overlapping (V,A,Lb,(Dn . Lb),n) & Ls = local_overlapping (V,A,Ln,(Ds . Ln),s) ) and
A4: j1 in dom d1 and
A5: b1 in dom d1 and
A6: n1 in dom d1 and
A7: s1 in dom d1 and
A8: d1 in dom Di and
A9: s <> i ; :: thesis:
A10: dom Dj = { d where d is NonatomicND of V,A : j1 in dom d } by A3, NOMIN_1:def 18;
A11: dom Db = { d where d is NonatomicND of V,A : b1 in dom d } by A3, NOMIN_1:def 18;
A12: dom Dn = { d where d is NonatomicND of V,A : n1 in dom d } by A3, NOMIN_1:def 18;
A13: dom Ds = { d where d is NonatomicND of V,A : s1 in dom d } by A3, NOMIN_1:def 18;
Di . d1 is TypeSCNominativeData of V,A by A8, PARTFUN1:4, NOMIN_1:39;
then A14: dom Li = {i} \/ (dom d1) by A1, A2, A3, NOMIN_4:4;
j1 in dom Li by A4, A14, XBOOLE_0:def 3;
then Li in dom Dj by A10;
then Dj . Li is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
then A15: dom Lj = {j} \/ (dom Li) by A1, A2, A3, NOMIN_4:4;
b1 in dom Li by A5, A14, XBOOLE_0:def 3;
then b1 in dom Lj by A15, XBOOLE_0:def 3;
then Lj in dom Db by A11;
then Db . Lj is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
then A16: dom Lb = {b} \/ (dom Lj) by A1, A2, A3, NOMIN_4:4;
n1 in dom Li by A6, A14, XBOOLE_0:def 3;
then n1 in dom Lj by A15, XBOOLE_0:def 3;
then n1 in dom Lb by A16, XBOOLE_0:def 3;
then Lb in dom Dn by A12;
then Dn . Lb is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
then A17: dom Ln = {n} \/ (dom Lb) by A1, A2, A3, NOMIN_4:4;
s1 in dom Li by A7, A14, XBOOLE_0:def 3;
then s1 in dom Lj by A15, XBOOLE_0:def 3;
then s1 in dom Lb by A16, XBOOLE_0:def 3;
then s1 in dom Ln by A17, XBOOLE_0:def 3;
then A18: Ln in dom Ds by A13;
i in {i} by TARSKI:def 1;
then i in dom Li by A14, XBOOLE_0:def 3;
then i in dom Lj by A15, XBOOLE_0:def 3;
then i in dom Lb by A16, XBOOLE_0:def 3;
then A19: i in dom Ln by A17, XBOOLE_0:def 3;
Ds . Ln is TypeSCNominativeData of V,A by A18, PARTFUN1:4, NOMIN_1:39;
hence Ls . i = Ln . i by A1, A2, A9, A19, A3, NOMIN_5:3; :: thesis: