let X, Y be finite natural-membered set ; :: thesis: ( X <> {} & X <N< Y implies (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 )
assume A1: ( X <> {} & X <N< Y ) ; :: thesis: (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0
A56v: card X <> 0 by A1;
0 < len (Sgm0 X) by A56v, Th44;
hence (Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0 by AE221, A1; :: thesis: verum