let n be 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 & q is nonnegative-yielding ) by A3;
then ( q = n --> 0 or ( q = {} & n = 0 ) ) by AFINSQ_2:74, A4;
then q = n --> 0 ;
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 AFINSQ_2:70, 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