let X, Y be finite natural-membered set ; ( Y <> {} & ex x being set st
( x in X & {x} <N= Y ) implies (Sgm0 X) . 0 <= (Sgm0 Y) . 0 )
assume that
A1:
Y <> {}
and
A2:
ex x being set st
( x in X & {x} <N= Y )
; (Sgm0 X) . 0 <= (Sgm0 Y) . 0
consider x being set such that
A3:
x in X
and
A4:
{x} <N= Y
by A2;
0 <> card Y
by A1;
then
0 < len (Sgm0 Y)
by Th20;
then A5:
0 in dom (Sgm0 Y)
by AFINSQ_1:86;
rng (Sgm0 Y) = Y
by Def4;
then A6:
(Sgm0 Y) . 0 in Y
by A5, FUNCT_1:def 3;
reconsider x0 = x as Element of NAT by A3, ORDINAL1:def 12;
set nx = x0;
x0 in {x0}
by TARSKI:def 1;
then A7:
x0 <= (Sgm0 Y) . 0
by A4, A6;
{x0} c= X
by A3, TARSKI:def 1;
then A8:
(Sgm0 X) . 0 <= (Sgm0 {x0}) . 0
by Th21;
(Sgm0 {x0}) . 0 = x0
by Th22;
hence
(Sgm0 X) . 0 <= (Sgm0 Y) . 0
by A8, A7, XXREAL_0:2; verum