let a, a1, v, v1, v2 be object ; :: thesis: for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))
let V, A be set ; :: thesis: ( {v,v1,v2} c= V & {a,a1} c= A implies ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) )
assume that
A1: {v,v1,v2} c= V and
A2: {a,a1} c= A ; :: thesis: ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))
v in {v,v1,v2} by ENUMSET1:def 1;
then A3: v in V by A1;
v1 in {v,v1,v2} by ENUMSET1:def 1;
then A4: v1 in V by A1;
A5: v2 in {v,v1,v2} by ENUMSET1:def 1;
A6: a in A by A2, ZFMISC_1:32;
A7: a1 in A by A2, ZFMISC_1:32;
set f = v2 .--> a1;
set g = ND_ex_4 (v,v1,v2,a,a1);
dom (ND_ex_4 (v,v1,v2,a,a1)) = {v,v1} by FUNCT_4:62;
then A8: dom (ND_ex_4 (v,v1,v2,a,a1)) c= V by A3, A4, TARSKI:def 2;
A9: rng (ND_ex_4 (v,v1,v2,a,a1)) c= {a,(v2 .--> a1)} by FUNCT_4:62;
rng (ND_ex_4 (v,v1,v2,a,a1)) c= A \/ (NDSS (V,A))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (ND_ex_4 (v,v1,v2,a,a1)) or x in A \/ (NDSS (V,A)) )
assume x in rng (ND_ex_4 (v,v1,v2,a,a1)) ; :: thesis: x in A \/ (NDSS (V,A))

per cases then ( x = a or x = v2 .--> a1 ) by A9, TARSKI:def 2;

suppose x = a ; :: thesis: x in A \/ (NDSS (V,A))

hence x in A \/ (NDSS (V,A)) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A10: x = v2 .--> a1 ; :: thesis: x in A \/ (NDSS (V,A))

A11: dom (v2 .--> a1) c= V by A1, A5, ZFMISC_1:31;
rng (v2 .--> a1) = {a1} by FUNCOP_1:8;
then rng (v2 .--> a1) c= A by A7, ZFMISC_1:31;
then v2 .--> a1 is PartFunc of V,A by A11, RELSET_1:4;
then v2 .--> a1 in NDSS (V,A) ;
hence x in A \/ (NDSS (V,A)) by A10, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then ND_ex_4 (v,v1,v2,a,a1) is PartFunc of V,(A \/ (NDSS (V,A))) by A8, RELSET_1:4;
hence ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A)))) ; :: thesis: verum