let V, A be set ; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st Seg 10 c= dom loc & loc is_valid_wrt d1 holds
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st Seg 10 c= dom loc & loc is_valid_wrt d1 holds
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1
let d1 be NonatomicND of V,A; :: thesis: ( Seg 10 c= dom loc & loc is_valid_wrt d1 implies {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1 )
assume that
A1: Seg 10 c= dom loc and
A2: rng loc c= dom d1 ; :: according to NOMIN_7:def 1 :: thesis: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set b = loc /. 5;
set c = loc /. 6;
set p = loc /. 7;
set q = loc /. 8;
set ps = loc /. 9;
set qc = loc /. 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} or x in dom d1 )
assume x in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} ; :: thesis: x in dom d1
then A3: ( x = loc /. 1 or x = loc /. 2 or x = loc /. 3 or x = loc /. 4 or x = loc /. 5 or x = loc /. 6 or x = loc /. 7 or x = loc /. 8 or x = loc /. 9 or x = loc /. 10 ) by ENUMSET1:def 8;
A4: 1 in Seg 10 & ... & 10 in Seg 10 ;
then A5: loc . 1 in rng loc & ... & loc . 10 in rng loc by A1, FUNCT_1:def 3;
loc . 1 = loc /. 1 & ... & loc . 10 = loc /. 10 by A1, A4, PARTFUN1:def 6;
hence x in dom d1 by A2, A3, A5; :: thesis: verum