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