let X, Y be finite natural-membered set ; :: thesis: ( X <> {} & X <N< Y implies (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 )
assume that
A1: X <> {} and
A2: X <N< Y ; :: thesis: (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0
card X <> 0 by A1;
then 0 < len (Sgm0 X) by Th20;
hence (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 by A2, Th29; :: thesis: verum