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 x in Domin_0 n,0 ; :: thesis: x in {(n --> 0 )}
then consider q being XFinSequence of NAT such that
A2: x = q and
q is dominated_by_0 and
A3: dom q = n and
A4: Sum q = 0 by Def2;
len q = n by A3;
then for x being set st x in dom q holds
q . x = 0 by A4, STIRL2_1:53;
then q = n --> 0 by A3, FUNCOP_1:17;
hence x in {(n --> 0 )} by A2, TARSKI:def 1; :: thesis: verum

end;

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

proof

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

end;

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