let n be Element of NAT ; :: thesis: Domin_0 n,0 = {(n --> 0 )}
set p = n --> 0 ;
A1: Domin_0 n,0 c= {(n --> 0 )}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Domin_0 n,0 or x in {(n --> 0 )} )
assume A2: x in Domin_0 n,0 ; :: thesis: x in {(n --> 0 )}
consider q being XFinSequence of such that
A3: ( x = q & q is dominated_by_0 & dom q = n & Sum q = 0 ) by A2, Def2;
len q = n by A3;
then for x being set st x in dom q holds
q . x = 0 by A3, STIRL2_1:53;
then q = n --> 0 by A3, FUNCOP_1:17;
hence x in {(n --> 0 )} by A3, TARSKI:def 1; :: thesis: verum

end;

{(n --> 0 )} c= Domin_0 n,0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(n --> 0 )} or x in Domin_0 n,0 )
assume A4: x in {(n --> 0 )} ; :: thesis: x in Domin_0 n,0
( dom (n --> 0 ) = n & Sum (n --> 0 ) = n * 0 & n --> 0 is dominated_by_0 ) by Lm2, Lm3, FUNCOP_1:19;
then n --> 0 in Domin_0 n,0 by Def2;
hence x in Domin_0 n,0 by A4, TARSKI:def 1; :: thesis: verum

end;

hence Domin_0 n,0 = {(n --> 0 )} by A1, XBOOLE_0:def 10; :: thesis: verum