let a1, v, v1 be object ; :: thesis: for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

let V, A be set ; :: thesis: ( {v,v1} c= V & a1 in A implies ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) )

assume that

A1: {v,v1} c= V and

A2: a1 in A ; :: thesis: ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

reconsider V1 = V, A1 = A as non empty set by A1, A2;

reconsider v = v, v1 = v1 as Element of V1 by A1, ZFMISC_1:32;

reconsider a1 = a1 as Element of A1 by A2;

set d = ND_ex_2 (v,v1,a1);

A3: dom (v .--> (v1 .--> a1)) c= V ;

A4: rng (ND_ex_2 (v,v1,a1)) = {(v1 .--> a1)} by FUNCOP_1:88;

v1 .--> a1 in NDSS (V,A) ;

then v1 .--> a1 in A \/ (NDSS (V,A)) by XBOOLE_0:def 3;

then rng (ND_ex_2 (v,v1,a1)) c= A \/ (NDSS (V,A)) by A4, ZFMISC_1:31;

then ND_ex_2 (v,v1,a1) is PartFunc of V,(A \/ (NDSS (V,A))) by A3, RELSET_1:4;

hence ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) ; :: thesis: verum

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

let V, A be set ; :: thesis: ( {v,v1} c= V & a1 in A implies ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) )

assume that

A1: {v,v1} c= V and

A2: a1 in A ; :: thesis: ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))

reconsider V1 = V, A1 = A as non empty set by A1, A2;

reconsider v = v, v1 = v1 as Element of V1 by A1, ZFMISC_1:32;

reconsider a1 = a1 as Element of A1 by A2;

set d = ND_ex_2 (v,v1,a1);

A3: dom (v .--> (v1 .--> a1)) c= V ;

A4: rng (ND_ex_2 (v,v1,a1)) = {(v1 .--> a1)} by FUNCOP_1:88;

v1 .--> a1 in NDSS (V,A) ;

then v1 .--> a1 in A \/ (NDSS (V,A)) by XBOOLE_0:def 3;

then rng (ND_ex_2 (v,v1,a1)) c= A \/ (NDSS (V,A)) by A4, ZFMISC_1:31;

then ND_ex_2 (v,v1,a1) is PartFunc of V,(A \/ (NDSS (V,A))) by A3, RELSET_1:4;

hence ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) ; :: thesis: verum