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 object ; :: 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 A4, AFINSQ_2:62;
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 Lm2;
( dom (n --> 0) = n & Sum (n --> 0) = n * 0 ) by AFINSQ_2:58;
then A6: n --> 0 in Domin_0 (n,0) by A5, Def2;
let x be object ; :: 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; :: thesis: verum