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