let X, Y be finite natural-membered set ; :: thesis: ( X c= Y & X <> {} implies (Sgm0 Y) . 0 <= (Sgm0 X) . 0 )
assume that
A1: X c= Y and
A2: X <> {} ; :: thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
reconsider X0 = X as finite set ;
0 <> card X0 by A2;
then 0 < len (Sgm0 X) by Th20;
then A3: 0 in dom (Sgm0 X) by AFINSQ_1:86;
A4: rng (Sgm0 Y) = Y by Def4;
rng (Sgm0 X) = X by Def4;
then (Sgm0 X) . 0 in X by A3, FUNCT_1:def 3;
then consider x being object such that
A5: x in dom (Sgm0 Y) and
A6: (Sgm0 Y) . x = (Sgm0 X) . 0 by A1, A4, FUNCT_1:def 3;
reconsider nx = x as Nat by A5;
A7: nx < len (Sgm0 Y) by A5, AFINSQ_1:86;
now :: thesis: ( ( 0 <> nx & (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ) or ( 0 = nx & (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ) )
per cases ( 0 <> nx or 0 = nx ) ;
case 0 <> nx ; :: thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6, A7, Def4; :: thesis: verum
end;
case 0 = nx ; :: thesis: (Sgm0 Y) . 0 <= (Sgm0 X) . 0
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 by A6; :: thesis: verum
end;
end;
end;
hence (Sgm0 Y) . 0 <= (Sgm0 X) . 0 ; :: thesis: verum